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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-tuff.opb
MD5SUM	06d4e815794ce4b5deed10c51066684b
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	60
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	3145725
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	6025434365952
Number of bits of the biggest number in a constraint	43
Biggest sum of numbers in a constraint	1078851036553950
Number of bits of the biggest sum of numbers	50
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.719889
Number of variables	11495
Total number of constraints	320
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	320
Minimum length of a constraint	8
Maximum length of a constraint	2240
Trace number 31066

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-05-25 21:44:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22458 boxname=wulflinc5 idbench=1274 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  06d4e815794ce4b5deed10c51066684b  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-tuff.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-tuff.opb
IDLAUNCH: 22458
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        620956 kB
Buffers:         34588 kB
Cached:         357572 kB
SwapCached:        472 kB
Active:         103656 kB
Inactive:       290572 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        620704 kB
SwapTotal:     2097136 kB
SwapFree:      2095792 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5228 kB
Slab:            13700 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:04:40 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22458 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 553 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ss
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   12
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   11
c ---[ 549]---> BDD-cost:   14
c ---[ 548]---> BDD-cost:   11
c ---[ 547]---> BDD-cost:   11
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    9
c ---[ 541]---> BDD-cost:   11
c ---[ 536]---> BDD-cost:   12
c ---[ 535]---> BDD-cost:   15
c ---[ 533]---> BDD-cost:   12
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:  778
c ---[ 525]---> BDD-cost:   64
c ---[ 521]---> Sorter-cost: 2214     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 519]---> BDD-cost:   54
c ---[ 517]---> BDD-cost:  863
c ---[ 513]---> BDD-cost:  931
c ---[ 511]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 509]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> BDD-cost:   40
c ---[ 499]---> BDD-cost:   51
c ---[ 495]---> BDD-cost:   51
c ---[ 493]---> BDD-cost:   40
c ---[ 491]---> BDD-cost:   53
c ---[ 487]---> BDD-cost:  225
c ---[ 485]---> BDD-cost:   40
c ---[ 483]---> BDD-cost:   51
c ---[ 479]---> BDD-cost:   51
c ---[ 477]---> BDD-cost:   51
c ---[ 475]---> Adder-cost: 509   maxlim: 2285382   bits: 23/22
c ---[ 473]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> BDD-cost:  114
c ---[ 467]---> BDD-cost:   36
c ---[ 463]---> BDD-cost:   36
c ---[ 461]---> BDD-cost:   36
c ---[ 459]---> BDD-cost:   40
c ---[ 455]---> BDD-cost:   36
c ---[ 451]---> BDD-cost:   36
c ---[ 449]---> Adder-cost: 985   maxlim: 8901434   bits: 25/24
c ---[ 447]---> Adder-cost: 318   maxlim: 350037   bits: 20/19
c ---[ 443]---> Sorter-cost:15513     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2
c ---[ 441]---> BDD-cost:  159
c ---[ 439]---> Sorter-cost: 2170     Base: 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> BDD-cost:   28
c ---[ 433]---> BDD-cost:   28
c ---[ 431]---> BDD-cost:   46
c ---[ 429]---> Sorter-cost: 3431     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 413]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Adder-cost: 552   maxlim: 2866973   bits: 23/22
c ---[ 391]---> Adder-cost: 433   maxlim: 2047827   bits: 22/21
c ---[ 389]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 5 2
c ---[ 387]---> Adder-cost: 2098   maxlim: 741739   bits: 20/20
c ---[ 385]---> Adder-cost: 9948   maxlim: 568059429   bits: 31/30
c ---[ 383]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Adder-cost: 2026   maxlim: 481643   bits: 19/19
c ---[ 379]---> Adder-cost: 9646   maxlim: 368774693   bits: 30/29
c ---[ 377]---> Sorter-cost: 1405     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 375]---> Adder-cost: 2026   maxlim: 481643   bits: 19/19
c ---[ 373]---> Adder-cost: 9646   maxlim: 368774693   bits: 30/29
c ---[ 371]---> Adder-cost: 2121   maxlim: 334037412   bits: 30/29
c ---[ 369]---> Adder-cost: 2214   maxlim: 105376178425   bits: 38/37
c ---[ 367]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost: 3132     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[ 361]---> BDD-cost:  327
c ---[ 359]---> Sorter-cost: 4437     Base: 2 2 2 2 5 2 2 2 2 2 2 2 3 2 2 2 2 2
c ---[ 357]---> BDD-cost:   86
c ---[ 355]---> BDD-cost:   25
c ---[ 351]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> BDD-cost:  105
c ---[ 347]---> Sorter-cost: 2036     Base: 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2
c ---[ 345]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Adder-cost: 1566   maxlim: 274942400   bits: 30/29
c ---[ 337]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost: 3193     Base: 2 2 2 2 2 2 13 2 2 2 3 2
c ---[ 331]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> BDD-cost:  116
c ---[ 325]---> BDD-cost:  109
c ---[ 323]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 319]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Adder-cost: 439   maxlim: 1164743   bits: 22/21
c ---[ 315]---> BDD-cost:   43
c ---[ 313]---> BDD-cost:  109
c ---[ 311]---> BDD-cost:  118
c ---[ 309]---> BDD-cost:  109
c ---[ 307]---> BDD-cost:  118
c ---[ 305]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 303]---> Sorter-cost:  547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> Sorter-cost:  508     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 299]---> Sorter-cost:  547     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 297]---> Adder-cost: 1981   maxlim: 449996839   bits: 30/29
c ---[ 295]---> Adder-cost: 2665   maxlim: 727026800   bits: 31/30
c ---[ 293]---> Adder-cost: 620   maxlim: 712644   bits: 21/20
c ---[ 291]---> Adder-cost: 326   maxlim: 270270   bits: 20/19
c ---[ 289]---> Sorter-cost: 1593     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 287]---> Sorter-cost: 3678     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 285]---> Sorter-cost: 2540     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> BDD-cost:  100
c ---[ 281]---> Adder-cost: 2138   maxlim: 1364267409   bits: 32/31
c ---[ 279]---> BDD-cost:   91
c ---[ 273]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 271]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 269]---> Sorter-cost: 5333     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 267]---> Sorter-cost: 5813     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 265]---> Adder-cost: 1114   maxlim: 422672800   bits: 30/29
c ---[ 263]---> BDD-cost:  275
c ---[ 261]---> BDD-cost:  301
c ---[ 259]---> Sorter-cost: 1710     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 3 3 2
c ---[ 257]---> Adder-cost: 1134   maxlim: 422672800   bits: 30/29
c ---[ 255]---> Sorter-cost: 5281     Base: 2 5 5 5 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 253]---> Sorter-cost: 2616     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 2911     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> BDD-cost:  397
c ---[ 241]---> Adder-cost: 1004   maxlim: 57748900   bits: 27/26
c ---[ 239]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 5 2
c ---[ 237]---> Sorter-cost: 1983     Base: 2 2 2 2 2 2 5 2 5 2 2 2 2
c ---[ 235]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 233]---> Sorter-cost: 2917     Base: 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 5
c ---[ 231]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 5
c ---[ 229]---> Sorter-cost: 2027     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 227]---> Sorter-cost: 2021     Base: 2 2 2 2 2 2 13 2 2 2 2 3 2
c ---[ 225]---> Adder-cost: 559   maxlim: 1826648   bits: 22/21
c ---[ 223]---> BDD-cost:  171
c ---[ 221]---> BDD-cost:   51
c ---[ 219]---> BDD-cost:   55
c ---[ 217]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  469     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> BDD-cost: 1013
c ---[ 185]---> Sorter-cost: 6016     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Adder-cost: 453   maxlim: 2965198   bits: 23/22
c ---[ 175]---> BDD-cost:   31
c ---[ 173]---> BDD-cost:   40
c ---[ 169]---> BDD-cost:   43
c ---[ 167]---> BDD-cost:   46
c ---[ 165]---> BDD-cost:   91
c ---[ 163]---> BDD-cost:  116
c ---[ 159]---> BDD-cost:  121
c ---[ 157]---> BDD-cost:  126
c ---[ 155]---> Sorter-cost: 2066     Base: 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 153]---> BDD-cost:  116
c ---[ 151]---> Sorter-cost:  988     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 2593     Base: 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> BDD-cost:  138
c ---[ 143]---> BDD-cost:  138
c ---[ 141]---> BDD-cost:  163
c ---[ 137]---> Adder-cost: 466   maxlim: 16383000   bits: 25/24
c ---[ 135]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   51
c ---[ 131]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost:  858     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost: 2533     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 125]---> Sorter-cost:  879     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 123]---> Sorter-cost: 1512     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 121]---> BDD-cost:   98
c ---[ 119]---> BDD-cost:   34
c ---[ 117]---> BDD-cost:  115
c ---[ 115]---> BDD-cost:   34
c ---[ 113]---> BDD-cost:   34
c ---[ 111]---> BDD-cost:   34
c ---[ 109]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost: 2196     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> BDD-cost:  137
c ---[ 101]---> Adder-cost: 320   maxlim: 262143   bits: 19/18
c ---[  99]---> Sorter-cost: 3786     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 5 5 3
c ---[  95]---> BDD-cost:  132
c ---[  93]---> BDD-cost:  132
c ---[  91]---> BDD-cost:  143
c ---[  88]---> Sorter-cost:  331     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  87]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Adder-cost: 6656   maxlim: 8191499   bits: 24/23/oldhome/oroussel/solvers/minisat+_script: line 9: 26600 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.78 0.92 0.95 2/54 26596
Raw data (stat): 26596 (runsolver) R 26595 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783993908 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.81 0.92 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.84 0.93 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0025 s]
Raw data (loadavg): 0.86 0.93 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0097 s]
Raw data (loadavg): 0.88 0.93 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0165 s]
Raw data (loadavg): 0.90 0.93 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0166 s]
Raw data (loadavg): 0.92 0.93 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0176 s]
Raw data (loadavg): 0.93 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0187 s]
Raw data (loadavg): 0.94 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0188 s]
Raw data (loadavg): 0.95 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.019 s]
Raw data (loadavg): 0.95 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.019 s]
Raw data (loadavg): 0.96 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.019 s]
Raw data (loadavg): 0.97 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.02 s]
Raw data (loadavg): 0.97 0.94 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.02 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.02 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.021 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.02 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.021 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.022 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.022 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.021 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.021 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.022 s]
Raw data (loadavg): 0.99 0.95 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.023 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.022 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 26600
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.022 s]
Raw data (loadavg): 1.07 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.022 s]
Raw data (loadavg): 1.06 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.022 s]
Raw data (loadavg): 1.05 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.022 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 26653
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.68 s]
Raw data (loadavg): 1.00 0.99 0.95 1/53 26655
Raw data (stat): 26596 (minisat+_script) S 26595 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783993908 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.68
CPU time (s): 1229.85
CPU user time (s): 1228.12
CPU system time (s): 1.72574
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####