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/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUM	c1b4c3ad409db732d2b559e570b6f24c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	138
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	819200
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	4941871
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	84
Trace number 16566

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        614324 kB
Buffers:         29656 kB
Cached:         368708 kB
SwapCached:        320 kB
Active:         113428 kB
Inactive:       287496 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        614072 kB
SwapTotal:     2097136 kB
SwapFree:      2096448 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5752 kB
Slab:            13704 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:05:04 (client local time) WITH STATUS 0 IN 1200.58 SECONDS
stats: 13140 7 1200.58 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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: 352   maxlim: 2411343   bits: 22/22
c ---[ 272]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 271]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 270]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 269]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 267]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 266]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 265]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 264]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 263]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 259]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 258]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 257]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 256]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 255]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 251]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 247]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 243]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 242]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 236]---> Adder-cost: 282   maxlim: 1636900   bits: 21/21
c ---[ 235]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 234]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 233]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 229]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 227]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 224]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 220]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 219]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 214]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 211]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 198]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 197]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 193]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 192]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 185]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 184]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 183]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 179]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 175]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 170]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 169]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 167]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 164]---> Adder-cost: 312   maxlim: 1842000   bits: 22/21
c ---[ 163]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 162]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 161]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 160]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 159]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 158]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 157]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 156]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 155]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 154]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 152]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 150]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 149]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 147]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 146]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 145]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 144]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 143]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 141]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 140]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 137]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 135]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 133]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 132]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 131]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 129]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 124]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 123]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 121]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 119]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 118]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 117]---> Adder-cost: 0   maxlim: 510   bits: 10/9
c ---[ 114]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 113]---> Adder-cost: 0   maxlim: 1022   bits: 11/10
c ---[ 112]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 110]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 109]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ---[ 107]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 105]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 103]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 101]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  99]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  97]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  95]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  93]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  91]---> Adder-cost: 394   maxlim: 1841200   bits: 22/21
c ---[  89]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[  87]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  85]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  83]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  81]---> Adder-cost: 316   maxlim: 2149200   bits: 22/22
c ---[  73]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  69]---> Adder-cost: 384   maxlim: 3377200   bits: 23/22
c ---[  66]---> Adder-cost: 272   maxlim: 402565   bits: 20/19
c ---[  65]---> Adder-cost: 444   maxlim: 658315   bits: 20/20
c ---[  64]---> Adder-cost: 454   maxlim: 722315   bits: 20/20
c ---[  63]---> Adder-cost: 534   maxlim: 914065   bits: 20/20
c ---[  62]---> Adder-cost: 754   maxlim: 1297940   bits: 21/21
c ---[  61]---> Adder-cost: 730   maxlim: 977940   bits: 21/20
c ---[  60]---> Adder-cost: 82   maxlim: 17141   bits: 15/15
c ---[  58]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[  57]---> Adder-cost: 156   maxlim: 27371   bits: 15/15
c ---[  56]---> Adder-cost: 164   maxlim: 29931   bits: 16/15
c ---[  55]---> Adder-cost: 210   maxlim: 32481   bits: 16/15
c ---[  54]---> Adder-cost: 266   maxlim: 42716   bits: 16/16
c ---[  53]---> Adder-cost: 270   maxlim: 45276   bits: 16/16
c ---[  52]---> Adder-cost: 80   maxlim: 18933   bits: 15/15
c ---[  51]---> Adder-cost: 162   maxlim: 29163   bits: 16/15
c ---[  50]---> Adder-cost: 156   maxlim: 30443   bits: 16/15
c ---[  49]---> Adder-cost: 210   maxlim: 38113   bits: 16/16
c ---[  48]---> Adder-cost: 268   maxlim: 48348   bits: 16/16
c ---[  46]---> Adder-cost: 258   maxlim: 1330100   bits: 21/21
c ---[  45]---> Adder-cost: 262   maxlim: 45788   bits: 16/16
c ---[  44]---> Adder-cost: 40   maxlim: 3965   bits: 13/12
c ---[  43]---> Adder-cost: 78   maxlim: 4987   bits: 13/13
c ---[  42]---> Adder-cost: 80   maxlim: 6267   bits: 13/13
c ---[  41]---> Adder-cost: 112   maxlim: 6521   bits: 13/13
c ---[  40]---> Adder-cost: 138   maxlim: 9592   bits: 14/14
c ---[  39]---> Adder-cost: 134   maxlim: 8056   bits: 14/13
c ---[  38]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[  33]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  30]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  24]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[  21]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  14]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  13]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[   9]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   4]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   0]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  128691   468095 |   42897       0        0     nan |  0.000 % |
c |       100 |  128691   468095 |   47186     100      357     3.6 | 19.006 % |
c |       251 |  128683   468069 |   51905     250      976     3.9 | 19.010 % |
c |       476 |  128675   468043 |   57095     474     3069     6.5 | 19.014 % |
c |       813 |  128668   468020 |   62805     810     6251     7.7 | 19.018 % |
c |      1319 |  128668   468020 |   69086    1316    15715    11.9 | 19.018 % |
c |      2078 |  128661   467997 |   75994    2073    29520    14.2 | 19.022 % |
c |      3217 |  128603   467805 |   83594    3206    39935    12.5 | 19.058 % |
c |      4925 |  128588   467758 |   91953    4913    69817    14.2 | 19.070 % |
c |      7487 |  128581   467734 |  101148    7474   149479    20.0 | 19.074 % |
c |     11332 |  128581   467734 |  111263   11319   245675    21.7 | 19.074 % |
c |     17099 |  128565   467680 |  122390   17081   382307    22.4 | 19.082 % |
c |     25749 |  128534   467577 |  134629   25724   630436    24.5 | 19.101 % |
c |     38723 |  128534   467577 |  148092   38698  1131256    29.2 | 19.101 % |
c |     58185 |  128534   467577 |  162901   58160  1701459    29.3 | 19.101 % |
c |     87378 |  128518   467525 |  179191   87351  2524227    28.9 | 19.113 % |
c |    131167 |  128400   467103 |  197110  131096  4443419    33.9 | 19.149 % |
c |    196853 |  128385   467058 |  216821  196779  6643770    33.8 | 19.161 % |
c |    295379 |  128359   466980 |  238503   92114  2776643    30.1 | 19.181 % |
c |    443168 |  128304   466795 |  262354  239893  7191120    30.0 | 19.212 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 10292
Raw data (stat): 10292 (runsolver) R 10291 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485158340 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 4188 0 0 0 990 9 0 0 25 0 1 0 485158340 19378176 4025 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4731 4025 603 41 0 4690 0
vsize: 18924
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 4821 0 0 0 1988 11 0 0 25 0 1 0 485158340 22052864 4658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5384 4658 603 41 0 5343 0
vsize: 21536
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5335 0 0 0 2987 12 0 0 25 0 1 0 485158340 24186880 5172 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5905 5172 603 41 0 5864 0
vsize: 23620
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5715 0 0 0 3985 14 0 0 25 0 1 0 485158340 25661440 5552 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6265 5552 603 41 0 6224 0
vsize: 25060
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5967 0 0 0 4985 14 0 0 25 0 1 0 485158340 26996736 5804 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6591 5804 603 41 0 6550 0
vsize: 26364
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6194 0 0 0 5985 15 0 0 25 0 1 0 485158340 27963392 6031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6827 6031 603 41 0 6786 0
vsize: 27308
[startup+70.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6377 0 0 0 6984 16 0 0 25 0 1 0 485158340 28647424 6214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6994 6214 603 41 0 6953 0
vsize: 27976
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6542 0 0 0 7984 16 0 0 25 0 1 0 485158340 29339648 6379 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7163 6379 603 41 0 7122 0
vsize: 28652
[startup+90.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7042 0 0 0 8983 18 0 0 25 0 1 0 485158340 31354880 6879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7655 6879 603 41 0 7614 0
vsize: 30620
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7501 0 0 0 9982 19 0 0 25 0 1 0 485158340 33239040 7338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8115 7338 603 41 0 8074 0
vsize: 32460
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7853 0 0 0 10982 20 0 0 25 0 1 0 485158340 34713600 7690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8475 7690 603 41 0 8434 0
vsize: 33900
[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8153 0 0 0 11982 21 0 0 25 0 1 0 485158340 35934208 7990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8773 7990 603 41 0 8732 0
vsize: 35092
[startup+130.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8459 0 0 0 12983 21 0 0 25 0 1 0 485158340 37175296 8296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8296 603 41 0 9035 0
vsize: 36304
[startup+140.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8666 0 0 0 13982 22 0 0 25 0 1 0 485158340 37994496 8503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9276 8503 603 41 0 9235 0
vsize: 37104
[startup+150.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8927 0 0 0 14982 23 0 0 25 0 1 0 485158340 39096320 8764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9545 8764 603 41 0 9504 0
vsize: 38180
[startup+160.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9230 0 0 0 15981 24 0 0 25 0 1 0 485158340 40964096 9067 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10001 9067 603 41 0 9960 0
vsize: 40004
[startup+170.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9572 0 0 0 16981 25 0 0 25 0 1 0 485158340 42295296 9409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10326 9409 603 41 0 10285 0
vsize: 41304
[startup+180.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9871 0 0 0 17980 26 0 0 25 0 1 0 485158340 43507712 9708 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10622 9708 603 41 0 10581 0
vsize: 42488
[startup+190.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10133 0 0 0 18980 27 0 0 25 0 1 0 485158340 44617728 9970 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10893 9970 603 41 0 10852 0
vsize: 43572
[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10387 0 0 0 19979 28 0 0 25 0 1 0 485158340 45633536 10224 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11141 10224 603 41 0 11100 0
vsize: 44564
[startup+210.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10568 0 0 0 20979 28 0 0 25 0 1 0 485158340 46305280 10405 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11305 10405 603 41 0 11264 0
vsize: 45220
[startup+220.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10718 0 0 0 21979 29 0 0 25 0 1 0 485158340 46977024 10555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11469 10555 603 41 0 11428 0
vsize: 45876
[startup+230.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10871 0 0 0 22979 29 0 0 25 0 1 0 485158340 47517696 10708 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11601 10708 603 41 0 11560 0
vsize: 46404
[startup+240.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11024 0 0 0 23979 30 0 0 25 0 1 0 485158340 48214016 10861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11771 10861 603 41 0 11730 0
vsize: 47084
[startup+250.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11156 0 0 0 24980 30 0 0 25 0 1 0 485158340 48750592 10993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 10993 603 41 0 11861 0
vsize: 47608
[startup+260.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11283 0 0 0 25980 31 0 0 25 0 1 0 485158340 49147904 11120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11999 11120 603 41 0 11958 0
vsize: 47996
[startup+270.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11409 0 0 0 26980 31 0 0 25 0 1 0 485158340 49680384 11246 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12129 11246 603 41 0 12088 0
vsize: 48516
[startup+280.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11524 0 0 0 27980 31 0 0 25 0 1 0 485158340 50216960 11361 4294967295 134512640 134672761 3221224544 3221223728 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12260 11361 603 41 0 12219 0
vsize: 49040
[startup+290.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11635 0 0 0 28981 32 0 0 25 0 1 0 485158340 50618368 11472 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12358 11472 603 41 0 12317 0
vsize: 49432
[startup+300.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11745 0 0 0 29981 32 0 0 25 0 1 0 485158340 51048448 11582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12463 11582 603 41 0 12422 0
vsize: 49852
[startup+310.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11967 0 0 0 30980 33 0 0 25 0 1 0 485158340 52031488 11804 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12703 11804 603 41 0 12662 0
vsize: 50812
[startup+320.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12221 0 0 0 31980 34 0 0 25 0 1 0 485158340 52977664 12058 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12934 12058 603 41 0 12893 0
vsize: 51736
[startup+330.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12481 0 0 0 32980 34 0 0 25 0 1 0 485158340 54054912 12318 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13197 12318 603 41 0 13156 0
vsize: 52788
[startup+340.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12709 0 0 0 33980 34 0 0 25 0 1 0 485158340 55005184 12546 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13429 12546 603 41 0 13388 0
vsize: 53716
[startup+350.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12880 0 0 0 34980 35 0 0 25 0 1 0 485158340 55693312 12717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13597 12717 603 41 0 13556 0
vsize: 54388
[startup+360.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12996 0 0 0 35981 36 0 0 25 0 1 0 485158340 56238080 12833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13730 12833 603 41 0 13689 0
vsize: 54920
[startup+370.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13088 0 0 0 36981 36 0 0 25 0 1 0 485158340 56643584 12925 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12925 603 41 0 13788 0
vsize: 55316
[startup+380.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13088 0 0 0 37982 36 0 0 25 0 1 0 485158340 56643584 12925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12925 603 41 0 13788 0
vsize: 55316
[startup+390.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13089 0 0 0 38982 36 0 0 25 0 1 0 485158340 56643584 12926 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12926 603 41 0 13788 0
vsize: 55316
[startup+400.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13090 0 0 0 39982 36 0 0 25 0 1 0 485158340 56643584 12927 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12927 603 41 0 13788 0
vsize: 55316
[startup+410.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 40983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+420.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 41983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+430.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 42983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+440.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 43984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+450.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 44984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+460.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 45984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+470.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 46985 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12930 603 41 0 13788 0
vsize: 55316
[startup+480.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 47985 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12932 603 41 0 13788 0
vsize: 55316
[startup+490.109 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 48986 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12932 603 41 0 13788 0
vsize: 55316
[startup+500.116 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 49987 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12932 603 41 0 13788 0
vsize: 55316
[startup+510.127 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13097 0 0 0 50988 36 0 0 25 0 1 0 485158340 56643584 12934 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12934 603 41 0 13788 0
vsize: 55316
[startup+520.127 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13097 0 0 0 51989 36 0 0 25 0 1 0 485158340 56643584 12934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12934 603 41 0 13788 0
vsize: 55316
[startup+530.127 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13098 0 0 0 52989 36 0 0 25 0 1 0 485158340 56643584 12935 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12935 603 41 0 13788 0
vsize: 55316
[startup+540.127 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13098 0 0 0 53989 36 0 0 25 0 1 0 485158340 56643584 12935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12935 603 41 0 13788 0
vsize: 55316
[startup+550.134 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13116 0 0 0 54990 36 0 0 25 0 1 0 485158340 56844288 12953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12953 603 41 0 13837 0
vsize: 55512
[startup+560.134 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13116 0 0 0 55991 36 0 0 25 0 1 0 485158340 56844288 12953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12953 603 41 0 13837 0
vsize: 55512
[startup+570.134 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13136 0 0 0 56991 36 0 0 25 0 1 0 485158340 56844288 12973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12973 603 41 0 13837 0
vsize: 55512
[startup+580.134 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 57991 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12976 603 41 0 13837 0
vsize: 55512
[startup+590.134 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 58992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12976 603 41 0 13837 0
vsize: 55512
[startup+600.134 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 59992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12976 603 41 0 13837 0
vsize: 55512
[startup+610.135 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 60992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13878 12976 603 41 0 13837 0
vsize: 55512
[startup+620.134 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13157 0 0 0 61993 36 0 0 25 0 1 0 485158340 57106432 12994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 12994 603 41 0 13901 0
vsize: 55768
[startup+630.135 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13158 0 0 0 62993 36 0 0 25 0 1 0 485158340 57106432 12995 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 12995 603 41 0 13901 0
vsize: 55768
[startup+640.135 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13159 0 0 0 63993 36 0 0 25 0 1 0 485158340 57106432 12996 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 12996 603 41 0 13901 0
vsize: 55768
[startup+650.135 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13165 0 0 0 64994 36 0 0 25 0 1 0 485158340 57106432 13002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13002 603 41 0 13901 0
vsize: 55768
[startup+660.135 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13182 0 0 0 65994 36 0 0 25 0 1 0 485158340 57106432 13019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13019 603 41 0 13901 0
vsize: 55768
[startup+670.141 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13185 0 0 0 66995 36 0 0 25 0 1 0 485158340 57106432 13022 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13022 603 41 0 13901 0
vsize: 55768
[startup+680.141 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13186 0 0 0 67995 36 0 0 25 0 1 0 485158340 57106432 13023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13023 603 41 0 13901 0
vsize: 55768
[startup+690.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13187 0 0 0 68996 36 0 0 25 0 1 0 485158340 57106432 13024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13024 603 41 0 13901 0
vsize: 55768
[startup+700.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13188 0 0 0 69996 36 0 0 25 0 1 0 485158340 57106432 13025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13942 13025 603 41 0 13901 0
vsize: 55768
[startup+710.146 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13235 0 0 0 70997 36 0 0 25 0 1 0 485158340 57368576 13072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14006 13072 603 41 0 13965 0
vsize: 56024
[startup+720.153 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13242 0 0 0 71998 36 0 0 25 0 1 0 485158340 57368576 13079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14006 13079 603 41 0 13965 0
vsize: 56024
[startup+730.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13243 0 0 0 72999 36 0 0 25 0 1 0 485158340 57368576 13080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14006 13080 603 41 0 13965 0
vsize: 56024
[startup+740.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13264 0 0 0 73999 36 0 0 25 0 1 0 485158340 57630720 13101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14070 13101 603 41 0 14029 0
vsize: 56280
[startup+750.16 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13272 0 0 0 74999 36 0 0 25 0 1 0 485158340 57630720 13109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14070 13109 603 41 0 14029 0
vsize: 56280
[startup+760.161 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13307 0 0 0 76000 36 0 0 25 0 1 0 485158340 57892864 13144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 13144 603 41 0 14093 0
vsize: 56536
[startup+770.162 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13308 0 0 0 77000 36 0 0 25 0 1 0 485158340 57892864 13145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 13145 603 41 0 14093 0
vsize: 56536
[startup+780.162 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13309 0 0 0 78000 36 0 0 25 0 1 0 485158340 57892864 13146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 13146 603 41 0 14093 0
vsize: 56536
[startup+790.168 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13373 0 0 0 79001 37 0 0 25 0 1 0 485158340 58089472 13210 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13210 603 41 0 14141 0
vsize: 56728
[startup+800.176 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13379 0 0 0 80002 37 0 0 25 0 1 0 485158340 58089472 13216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13216 603 41 0 14141 0
vsize: 56728
[startup+810.176 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13381 0 0 0 81003 37 0 0 25 0 1 0 485158340 58089472 13218 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13218 603 41 0 14141 0
vsize: 56728
[startup+820.176 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13382 0 0 0 82003 37 0 0 25 0 1 0 485158340 58089472 13219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13219 603 41 0 14141 0
vsize: 56728
[startup+830.176 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13382 0 0 0 83003 37 0 0 25 0 1 0 485158340 58089472 13219 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13219 603 41 0 14141 0
vsize: 56728
[startup+840.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13385 0 0 0 84004 37 0 0 25 0 1 0 485158340 58089472 13222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13222 603 41 0 14141 0
vsize: 56728
[startup+850.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 85005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13223 603 41 0 14141 0
vsize: 56728
[startup+860.183 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 86005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13223 603 41 0 14141 0
vsize: 56728
[startup+870.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 87005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13223 603 41 0 14141 0
vsize: 56728
[startup+880.186 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 88006 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13223 603 41 0 14141 0
vsize: 56728
[startup+890.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 89006 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14182 13223 603 41 0 14141 0
vsize: 56728
[startup+900.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 10292
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 90007 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13232 603 41 0 14189 0
vsize: 56920
[startup+910.187 s]
Raw data (loadavg): 1.15 1.02 0.93 3/57 10328
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 91006 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13232 603 41 0 14189 0
vsize: 56920
[startup+920.187 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 92006 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13232 603 41 0 14189 0
vsize: 56920
[startup+930.187 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13409 0 0 0 93007 37 0 0 25 0 1 0 485158340 58286080 13246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13246 603 41 0 14189 0
vsize: 56920
[startup+940.188 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 94007 37 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13248 603 41 0 14189 0
vsize: 56920
[startup+950.188 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 95007 38 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13248 603 41 0 14189 0
vsize: 56920
[startup+960.189 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 96007 38 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13248 603 41 0 14189 0
vsize: 56920
[startup+970.196 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13413 0 0 0 97008 38 0 0 25 0 1 0 485158340 58286080 13250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13250 603 41 0 14189 0
vsize: 56920
[startup+980.203 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 10345
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13415 0 0 0 98009 38 0 0 25 0 1 0 485158340 58286080 13252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13252 603 41 0 14189 0
vsize: 56920
[startup+990.207 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13415 0 0 0 99010 38 0 0 25 0 1 0 485158340 58286080 13252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13252 603 41 0 14189 0
vsize: 56920
[startup+1000.21 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13457 0 0 0 100010 38 0 0 25 0 1 0 485158340 58482688 13294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14278 13294 603 41 0 14237 0
vsize: 57112
[startup+1010.21 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13459 0 0 0 101010 38 0 0 25 0 1 0 485158340 58482688 13296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14278 13296 603 41 0 14237 0
vsize: 57112
[startup+1020.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13461 0 0 0 102011 38 0 0 25 0 1 0 485158340 58482688 13298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14278 13298 603 41 0 14237 0
vsize: 57112
[startup+1030.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13463 0 0 0 103011 38 0 0 25 0 1 0 485158340 58482688 13300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14278 13300 603 41 0 14237 0
vsize: 57112
[startup+1040.21 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13464 0 0 0 104011 38 0 0 25 0 1 0 485158340 58482688 13301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14278 13301 603 41 0 14237 0
vsize: 57112
[startup+1050.21 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13487 0 0 0 105012 38 0 0 25 0 1 0 485158340 58744832 13324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13324 603 41 0 14301 0
vsize: 57368
[startup+1060.21 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13489 0 0 0 106012 38 0 0 25 0 1 0 485158340 58744832 13326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13326 603 41 0 14301 0
vsize: 57368
[startup+1070.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13491 0 0 0 107012 38 0 0 25 0 1 0 485158340 58744832 13328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13328 603 41 0 14301 0
vsize: 57368
[startup+1080.21 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13492 0 0 0 108013 38 0 0 25 0 1 0 485158340 58744832 13329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13329 603 41 0 14301 0
vsize: 57368
[startup+1090.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13495 0 0 0 109013 38 0 0 25 0 1 0 485158340 58744832 13332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13332 603 41 0 14301 0
vsize: 57368
[startup+1100.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13497 0 0 0 110013 38 0 0 25 0 1 0 485158340 58744832 13334 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13334 603 41 0 14301 0
vsize: 57368
[startup+1110.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13532 0 0 0 111014 38 0 0 25 0 1 0 485158340 59006976 13369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14406 13369 603 41 0 14365 0
vsize: 57624
[startup+1120.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13534 0 0 0 112014 38 0 0 25 0 1 0 485158340 59006976 13371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14406 13371 603 41 0 14365 0
vsize: 57624
[startup+1130.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13630 0 0 0 113014 38 0 0 25 0 1 0 485158340 59498496 13467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14526 13467 603 41 0 14485 0
vsize: 58104
[startup+1140.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13664 0 0 0 114014 38 0 0 25 0 1 0 485158340 59691008 13501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14573 13501 603 41 0 14532 0
vsize: 58292
[startup+1150.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13724 0 0 0 115014 39 0 0 25 0 1 0 485158340 59977728 13561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14643 13561 603 41 0 14602 0
vsize: 58572
[startup+1160.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13779 0 0 0 116014 39 0 0 25 0 1 0 485158340 60112896 13616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14676 13616 603 41 0 14635 0
vsize: 58704
[startup+1170.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13837 0 0 0 117014 39 0 0 25 0 1 0 485158340 60375040 13674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14740 13674 603 41 0 14699 0
vsize: 58960
[startup+1180.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13907 0 0 0 118014 39 0 0 25 0 1 0 485158340 60641280 13744 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14805 13744 603 41 0 14764 0
vsize: 59220
[startup+1190.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13961 0 0 0 119015 39 0 0 25 0 1 0 485158340 60903424 13798 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14869 13798 603 41 0 14828 0
vsize: 59476
[startup+1200.21 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 10347
Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 14014 0 0 0 120014 40 0 0 25 0 1 0 485158340 61034496 13851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14901 13851 603 41 0 14860 0
vsize: 59604
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 10347
Raw data (stat): 10292 (minisat+) Z 10291 29653 29652 0 -1 12 14016 0 0 0 120014 42 0 0 25 0 1 0 485158340 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.24
CPU time (s): 1200.58
CPU user time (s): 1200.15
CPU system time (s): 0.429934
CPU usage (%): 100.028
Max. virtual memory (Kb): 59604
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####