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-degen2.opb
MD5SUM	30256c883dd8af773c334a2b26410bd9
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	9400
Biggest coefficient in the objective function	2494038016
Number of bits for the biggest coefficient in the objective function	32
Sum of the numbers in the objective function	391862963250
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	2494038016
Number of bits of the biggest number in a constraint	32
Biggest sum of numbers in a constraint	391862963250
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.092985
Number of variables	10680
Total number of constraints	444
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	40
Maximum length of a constraint	1700
Trace number 20058

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        434032 kB
Buffers:         34780 kB
Cached:         538356 kB
SwapCached:        104 kB
Active:         209112 kB
Inactive:       366424 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        433780 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19448 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 20:22:05 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 15690 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 665 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[ 667]---> BDD-cost:59412
c ---[ 666]---> BDD-cost:52284
c ---[ 665]---> BDD-cost:32923
c ---[ 663]---> BDD-cost: 1280
c ---[ 661]---> BDD-cost: 1280
c ---[ 659]---> BDD-cost: 2580
c ---[ 657]---> BDD-cost: 2579
c ---[ 655]---> BDD-cost:  302
c ---[ 653]---> BDD-cost:  302
c ---[ 651]---> BDD-cost:  866
c ---[ 649]---> BDD-cost:  866
c ---[ 647]---> BDD-cost: 9173
c ---[ 645]---> BDD-cost:10298
c ---[ 643]---> BDD-cost:  866
c ---[ 641]---> BDD-cost:  866
c ---[ 639]---> BDD-cost: 3943
c ---[ 637]---> BDD-cost: 3943
c ---[ 635]---> BDD-cost:  564
c ---[ 633]---> BDD-cost:  564
c ---[ 631]---> BDD-cost: 3943
c ---[ 629]---> BDD-cost: 4330
c ---[ 627]---> BDD-cost:   22
c ---[ 625]---> BDD-cost: 1746
c ---[ 623]---> BDD-cost: 1746
c ---[ 621]---> BDD-cost:15125
c ---[ 619]---> BDD-cost:13684
c ---[ 617]---> BDD-cost:  302
c ---[ 615]---> BDD-cost:  302
c ---[ 613]---> BDD-cost:  302
c ---[ 611]---> BDD-cost:  301
c ---[ 609]---> BDD-cost:25312
c ---[ 607]---> BDD-cost:26347
c ---[ 605]---> BDD-cost:  302
c ---[ 603]---> BDD-cost:  302
c ---[ 601]---> BDD-cost: 1280
c ---[ 599]---> BDD-cost: 1280
c ---[ 597]---> BDD-cost:  302
c ---[ 595]---> BDD-cost:  302
c ---[ 593]---> BDD-cost:  128
c ---[ 591]---> BDD-cost:  128
c ---[ 589]---> BDD-cost:  302
c ---[ 587]---> BDD-cost:  302
c ---[ 585]---> BDD-cost: 2316
c ---[ 583]---> BDD-cost: 2316
c ---[ 581]---> BDD-cost: 8706
c ---[ 579]---> BDD-cost: 9308
c ---[ 577]---> BDD-cost:   64
c ---[ 576]---> BDD-cost:  131
c ---[ 575]---> BDD-cost:  130
c ---[ 574]---> BDD-cost:  130
c ---[ 573]---> BDD-cost:  316
c ---[ 572]---> BDD-cost:  315
c ---[ 571]---> BDD-cost:  315
c ---[ 570]---> BDD-cost:  558
c ---[ 569]---> BDD-cost:  557
c ---[ 568]---> BDD-cost:  557
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> BDD-cost:  128
c ---[ 565]---> BDD-cost:   67
c ---[ 564]---> BDD-cost:   67
c ---[ 563]---> BDD-cost:  565
c ---[ 562]---> BDD-cost:  434
c ---[ 561]---> BDD-cost:  205
c ---[ 560]---> BDD-cost:  895
c ---[ 559]---> BDD-cost:  708
c ---[ 558]---> BDD-cost:   68
c ---[ 557]---> BDD-cost:   67
c ---[ 556]---> BDD-cost:   67
c ---[ 555]---> BDD-cost:   68
c ---[ 554]---> BDD-cost:   67
c ---[ 553]---> BDD-cost:   67
c ---[ 552]---> BDD-cost:  200
c ---[ 551]---> BDD-cost:  199
c ---[ 550]---> BDD-cost:  205
c ---[ 549]---> BDD-cost:  422
c ---[ 548]---> BDD-cost:  421
c ---[ 547]---> BDD-cost:  425
c ---[ 546]---> BDD-cost:  435
c ---[ 545]---> BDD-cost:  424
c ---[ 544]---> BDD-cost:  434
c ---[ 543]---> BDD-cost: 1110
c ---[ 542]---> BDD-cost: 1100
c ---[ 541]---> BDD-cost: 1109
c ---[ 540]---> BDD-cost: 1821
c ---[ 539]---> BDD-cost: 2067
c ---[ 538]---> BDD-cost: 2080
c ---[ 537]---> BDD-cost: 2392
c ---[ 536]---> BDD-cost: 2690
c ---[ 535]---> BDD-cost: 2705
c ---[ 534]---> BDD-cost: 4147
c ---[ 533]---> BDD-cost: 4940
c ---[ 532]---> BDD-cost: 4965
c ---[ 531]---> BDD-cost: 5443
c ---[ 530]---> BDD-cost: 6317
c ---[ 529]---> BDD-cost: 6342
c ---[ 528]---> BDD-cost: 6426
c ---[ 527]---> BDD-cost: 7372
c ---[ 526]---> BDD-cost: 7399
c ---[ 525]---> BDD-cost: 7354
c ---[ 524]---> BDD-cost: 8400
c ---[ 523]---> BDD-cost: 8443
c ---[ 522]---> BDD-cost:   68
c ---[ 521]---> BDD-cost:   67
c ---[ 520]---> BDD-cost:   67
c ---[ 519]---> BDD-cost:  206
c ---[ 518]---> BDD-cost:  205
c ---[ 517]---> BDD-cost:  205
c ---[ 516]---> BDD-cost:  435
c ---[ 515]---> BDD-cost:  434
c ---[ 514]---> BDD-cost:  434
c ---[ 513]---> BDD-cost:  318
c ---[ 512]---> BDD-cost:  317
c ---[ 511]---> BDD-cost:  581
c ---[ 510]---> BDD-cost:  580
c ---[ 509]---> BDD-cost:   67
c ---[ 508]---> BDD-cost:  205
c ---[ 507]---> BDD-cost: 1140
c ---[ 506]---> BDD-cost: 1139
c ---[ 505]---> BDD-cost:  310
c ---[ 504]---> BDD-cost: 2123
c ---[ 503]---> BDD-cost: 2122
c ---[ 502]---> BDD-cost:  564
c ---[ 501]---> BDD-cost: 2725
c ---[ 500]---> BDD-cost: 2724
c ---[ 499]---> BDD-cost:  200
c ---[ 498]---> BDD-cost:  199
c ---[ 497]---> BDD-cost:   68
c ---[ 496]---> BDD-cost:   67
c ---[ 495]---> BDD-cost:  711
c ---[ 494]---> BDD-cost:  710
c ---[ 493]---> BDD-cost: 1299
c ---[ 492]---> BDD-cost: 1522
c ---[ 491]---> BDD-cost:  119
c ---[ 490]---> BDD-cost:   68
c ---[ 489]---> BDD-cost:   67
c ---[ 488]---> BDD-cost:   67
c ---[ 487]---> BDD-cost:  204
c ---[ 486]---> BDD-cost:  203
c ---[ 485]---> BDD-cost:  205
c ---[ 484]---> BDD-cost:  429
c ---[ 483]---> BDD-cost:  428
c ---[ 482]---> BDD-cost:  434
c ---[ 481]---> BDD-cost:  696
c ---[ 480]---> BDD-cost:  695
c ---[ 479]---> BDD-cost:  701
c ---[ 478]---> BDD-cost: 1072
c ---[ 477]---> BDD-cost: 1071
c ---[ 476]---> BDD-cost: 1073
c ---[ 475]---> BDD-cost:  120
c ---[ 474]---> BDD-cost:  127
c ---[ 473]---> BDD-cost:  517
c ---[ 472]---> BDD-cost:  537
c ---[ 471]---> BDD-cost: 1014
c ---[ 470]---> BDD-cost:   67
c ---[ 469]---> BDD-cost:  203
c ---[ 468]---> BDD-cost: 2338
c ---[ 467]---> BDD-cost: 2034
c ---[ 466]---> BDD-cost: 2879
c ---[ 465]---> BDD-cost: 2599
c ---[ 464]---> BDD-cost:  434
c ---[ 463]---> BDD-cost: 3659
c ---[ 462]---> BDD-cost: 4092
c ---[ 461]---> BDD-cost: 5239
c ---[ 460]---> BDD-cost: 4762
c ---[ 459]---> BDD-cost:  875
c ---[ 458]---> BDD-cost: 8118
c ---[ 457]---> BDD-cost: 9314
c ---[ 456]---> BDD-cost: 8713
c ---[ 455]---> BDD-cost:   66
c ---[ 454]---> BDD-cost:   65
c ---[ 453]---> BDD-cost:   67
c ---[ 452]---> BDD-cost:  204
c ---[ 451]---> BDD-cost:  203
c ---[ 450]---> BDD-cost:  203
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:  130
c ---[ 447]---> BDD-cost:   68
c ---[ 446]---> BDD-cost:  127
c ---[ 445]---> BDD-cost:  313
c ---[ 442]---> BDD-cost:  190
c ---[ 441]---> BDD-cost:  202
c ---[ 440]---> BDD-cost:  127
c ---[ 439]---> BDD-cost: 1355
c ---[ 438]---> BDD-cost:  939
c ---[ 437]---> BDD-cost: 1356
c ---[ 436]---> BDD-cost: 1831
c ---[ 435]---> BDD-cost: 1355
c ---[ 434]---> BDD-cost: 3080
c ---[ 433]---> BDD-cost: 3464
c ---[ 432]---> BDD-cost: 2744
c ---[ 431]---> BDD-cost: 3784
c ---[ 430]---> BDD-cost: 4169
c ---[ 429]---> BDD-cost: 4912
c ---[ 428]---> BDD-cost: 5824
c ---[ 427]---> BDD-cost: 6406
c ---[ 426]---> BDD-cost: 4995
c ---[ 425]---> BDD-cost: 5269
c ---[ 424]---> BDD-cost: 7933
c ---[ 423]---> BDD-cost: 8563
c ---[ 422]---> BDD-cost: 7008
c ---[ 421]---> BDD-cost:11719
c ---[ 420]---> BDD-cost:12366
c ---[ 419]---> BDD-cost: 9726
c ---[ 418]---> BDD-cost:15879
c ---[ 417]---> BDD-cost:16633
c ---[ 416]---> BDD-cost:13571
c ---[ 415]---> BDD-cost:18390
c ---[ 414]---> BDD-cost:19057
c ---[ 413]---> BDD-cost:15905
c ---[ 412]---> BDD-cost:20892
c ---[ 411]---> BDD-cost:21722
c ---[ 410]---> BDD-cost:18260
c ---[ 409]---> BDD-cost:   27
c ---[ 408]---> BDD-cost:  131
c ---[ 407]---> BDD-cost:   67
c ---[ 406]---> BDD-cost:   67
c ---[ 405]---> BDD-cost:   68
c ---[ 404]---> BDD-cost:   67
c ---[ 403]---> BDD-cost:  206
c ---[ 402]---> BDD-cost:  205
c ---[ 401]---> BDD-cost:  435
c ---[ 400]---> BDD-cost:  434
c ---[ 399]---> BDD-cost:   68
c ---[ 398]---> BDD-cost:   67
c ---[ 397]---> BDD-cost:  206
c ---[ 396]---> BDD-cost:  205
c ---[ 395]---> BDD-cost:   67
c ---[ 394]---> BDD-cost:   68
c ---[ 393]---> BDD-cost:   67
c ---[ 392]---> BDD-cost:   67
c ---[ 391]---> BDD-cost:   66
c ---[ 390]---> BDD-cost:   65
c ---[ 389]---> BDD-cost:   67
c ---[ 388]---> BDD-cost:    0
c ---[ 387]---> BDD-cost:  202
c ---[ 386]---> BDD-cost:  201
c ---[ 385]---> BDD-cost:  203
c ---[ 384]---> BDD-cost:   68
c ---[ 383]---> BDD-cost:   67
c ---[ 382]---> BDD-cost:   67
c ---[ 381]---> BDD-cost:  204
c ---[ 380]---> BDD-cost:  203
c ---[ 379]---> BDD-cost:  551
c ---[ 378]---> BDD-cost:  550
c ---[ 377]---> BDD-cost:  299
c ---[ 376]---> BDD-cost:   67
c ---[ 374]---> BDD-cost:  131
c ---[ 373]---> BDD-cost:  205
c ---[ 372]---> BDD-cost:  130
c ---[ 371]---> BDD-cost: 1090
c ---[ 370]---> BDD-cost: 1298
c ---[ 369]---> BDD-cost: 1825
c ---[ 368]---> BDD-cost: 2097
c ---[ 367]---> BDD-cost: 2373
c ---[ 366]---> BDD-cost: 2631
c ---[ 365]---> BDD-cost:  432
c ---[ 364]---> BDD-cost: 2954
c ---[ 363]---> BDD-cost: 3300
c ---[ 362]---> BDD-cost: 5984
c ---[ 361]---> BDD-cost: 6164
c ---[ 360]---> BDD-cost: 6805
c ---[ 359]---> BDD-cost: 6932
c ---[ 358]---> BDD-cost:   65
c ---[ 357]---> BDD-cost:   67
c ---[ 355]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   35
c ---[ 343]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   35
c ---[ 333]---> BDD-cost:   35
c ---[ 331]---> BDD-cost:   35
c ---[ 329]---> BDD-cost:   35
c ---[ 327]---> BDD-cost:   35
c ---[ 325]---> BDD-cost:   35
c ---[ 323]---> BDD-cost:   35
c ---[ 321]---> BDD-cost:   35
c ---[ 319]---> BDD-cost:   76
c ---[ 317]---> BDD-cost:   76
c ---[ 315]---> BDD-cost:   35
c ---[ 313]---> BDD-cost:   35
c ---[ 311]---> BDD-cost:   35
c ---[ 309]---> BDD-cost:   35
c ---[ 307]---> BDD-cost:   35
c ---[ 305]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   35
c ---[ 301]---> BDD-cost:   35
c ---[ 299]---> BDD-cost:   35
c ---[ 297]---> BDD-cost:   35
c ---[ 295]---> BDD-cost:   35
c ---[ 293]---> BDD-cost:   35
c ---[ 291]---> BDD-cost:   76
c ---[ 289]---> BDD-cost:   35
c ---[ 287]---> BDD-cost:   35
c ---[ 285]---> BDD-cost:   35
c ---[ 283]---> BDD-cost:   35
c ---[ 281]---> BDD-cost:   35
c ---[ 279]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   35
c ---[ 275]---> BDD-cost:   35
c ---[ 273]---> BDD-cost:   35
c ---[ 271]---> BDD-cost:   35
c ---[ 269]---> BDD-cost:   35
c ---[ 267]---> BDD-cost:   35
c ---[ 265]---> BDD-cost:   35
c ---[ 263]---> BDD-cost:   35
c ---[ 261]---> BDD-cost:   35
c ---[ 259]---> BDD-cost:   35
c ---[ 257]---> BDD-cost:   35
c ---[ 255]---> BDD-cost:   35
c ---[ 253]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   35
c ---[ 247]---> BDD-cost:   35
c ---[ 245]---> BDD-cost:   35
c ---[ 243]---> BDD-cost:   35
c ---[ 241]---> BDD-cost:   35
c ---[ 239]---> BDD-cost:   35
c ---[ 237]---> BDD-cost:   76
c ---[ 235]---> BDD-cost:   76
c ---[ 233]---> BDD-cost:   76
c ---[ 231]---> BDD-cost:   76
c ---[ 229]---> BDD-cost:   76
c ---[ 227]---> BDD-cost:   76
c ---[ 225]---> BDD-cost:   76
c ---[ 223]---> BDD-cost:   76
c ---[ 221]---> BDD-cost:   76
c ---[ 219]---> BDD-cost:   76
c ---[ 217]---> BDD-cost:   76
c ---[ 215]---> BDD-cost:   76
c ---[ 213]---> BDD-cost:   76
c ---[ 211]---> BDD-cost:   76
c ---[ 209]---> BDD-cost:   76
c ---[ 207]---> BDD-cost:   76
c ---[ 205]---> BDD-cost:   76
c ---[ 203]---> BDD-cost:   76
c ---[ 201]---> BDD-cost:   76
c ---[ 199]---> BDD-cost:   76
c ---[ 197]---> BDD-cost:   76
c ---[ 195]---> BDD-cost:   76
c ---[ 193]---> BDD-cost:   76
c ---[ 191]---> BDD-cost:   76
c ---[ 189]---> BDD-cost:   76
c ---[ 187]---> BDD-cost:   76
c ---[ 185]---> BDD-cost:   76
c ---[ 183]---> BDD-cost:   76
c ---[ 181]---> BDD-cost:   76
c ---[ 179]---> BDD-cost:   76
c ---[ 177]---> BDD-cost:   76
c ---[ 175]---> BDD-cost:   76
c ---[ 173]---> BDD-cost:   76
c ---[ 171]---> BDD-cost:   76
c ---[ 169]---> BDD-cost:   76
c ---[ 167]---> BDD-cost:   76
c ---[ 165]---> BDD-cost:   35
c ---[ 163]---> BDD-cost:   76
c ---[ 161]---> BDD-cost:   76
c ---[ 159]---> BDD-cost:   76
c ---[ 157]---> BDD-cost:   76
c ---[ 155]---> BDD-cost:   76
c ---[ 153]---> BDD-cost:   76
c ---[ 151]---> BDD-cost:   76
c ---[ 149]---> BDD-cost:   76
c ---[ 147]---> BDD-cost:   76
c ---[ 145]---> BDD-cost:   76
c ---[ 143]---> BDD-cost:   76
c ---[ 141]---> BDD-cost:   76
c ---[ 139]---> BDD-cost:   76
c ---[ 137]---> BDD-cost:   76
c ---[ 135]---> BDD-cost:   76
c ---[ 133]---> BDD-cost:   76
c ---[ 131]---> BDD-cost:   76
c ---[ 129]---> BDD-cost:   76
c ---[ 127]---> BDD-cost:   76
c ---[ 125]---> BDD-cost:   76
c ---[ 123]---> BDD-cost:   76
c ---[ 121]---> BDD-cost:   76
c ---[ 119]---> BDD-cost:   76
c ---[ 117]---> BDD-cost:   76
c ---[ 115]---> BDD-cost:   76
c ---[ 113]---> BDD-cost:   76
c ---[ 111]---> BDD-cost:   35
c ---[ 109]---> BDD-cost:   76
c ---[ 107]---> BDD-cost:   76
c ---[ 105]---> BDD-cost:   76
c ---[ 103]---> BDD-cost:   76
c ---[ 101]---> BDD-cost:   76
c ---[  99]---> BDD-cost:   76
c ---[  97]---> BDD-cost:   76
c ---[  95]---> BDD-cost:   76
c ---[  93]---> BDD-cost:   76
c ---[  91]---> BDD-cost:   76
c ---[  89]---> BDD-cost:   76
c ---[  87]---> BDD-cost:   76
c ---[  85]---> BDD-cost:   76
c ---[  83]---> BDD-cost:   76
c ---[  81]---> BDD-cost:   76
c ---[  79]---> BDD-cost:   76
c ---[  77]---> BDD-cost:   76
c ---[  75]---> BDD-cost:   76
c ---[  73]---> BDD-cost:   76
c ---[  71]---> BDD-cost:   76
c ---[  69]---> BDD-cost:   76
c ---[  67]---> BDD-cost:   76
c ---[  65]---> BDD-cost:   76
c ---[  63]---> BDD-cost:   76
c ---[  61]---> BDD-cost:   76
c ---[  59]---> BDD-cost:   76
c ---[  57]---> BDD-cost:   76
c ---[  55]---> BDD-cost:   76
c ---[  53]---> BDD-cost:   76
c ---[  51]---> BDD-cost:   76
c ---[  49]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  41]---> BDD-cost:   76
c ---[  39]---> BDD-cost:   76
c ---[  37]---> BDD-cost:   76
c ---[  35]---> BDD-cost:   76
c ---[  33]---> BDD-cost:   76
c ---[  31]---> BDD-cost:   35
c ---[  29]---> BDD-cost:   35
c ---[  27]---> BDD-cost:   76
c ---[  25]---> BDD-cost:   76
c ---[  23]---> BDD-cost:   76
c ---[  21]---> BDD-cost:   76
c ---[  19]---> BDD-cost:   76
c ---[  17]---> BDD-cost:   76
c ---[  15]---> BDD-cost:   76
c ---[  13]---> BDD-cost:   76
c ---[  11]---> BDD-cost:   76
c ---[   9]---> BDD-cost:   76
c ---[   7]---> BDD-cost:   76
c ---[   5]---> BDD-cost:   76
c ---[   3]---> BDD-cost:   76
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2410614  7168880 |  803538       0        0     nan |  0.000 % |
c |       101 | 2410614  7168880 |  883891     101    10956   108.5 |  0.786 % |
c |       251 | 2410614  7168880 |  972280     251    21407    85.3 |  0.786 % |
c |       476 | 2410614  7168880 | 1069509     476    40969    86.1 |  0.786 % |
c |       813 | 2410614  7168880 | 1176459     813    93260   114.7 |  0.786 % |
c |      1320 | 2410614  7168880 | 1294105    1320   127714    96.8 |  0.786 % |
c |      2079 | 2410614  7168880 | 1423516    2079   156326    75.2 |  0.786 % |
c |      3218 | 2410614  7168880 | 1565868    3218   449961   139.8 |  0.786 % |
c |      4927 | 2410614  7168880 | 1722455    4927   598838   121.5 |  0.786 % |
c |      7489 | 2410614  7168880 | 1894700    7489   881743   117.7 |  0.786 % |
c |     11333 | 2410614  7168880 | 2084170   11333  1519724   134.1 |  0.786 % |
c |     17100 | 2410614  7168880 | 2292587   17100  2336554   136.6 |  0.786 % |
c |     25750 | 2410614  7168880 | 2521846   25750  4604678   178.8 |  0.786 % |
c |     38724 | 2410614  7168880 | 2774031   38724  5233095   135.1 |  0.786 % |
c |     58187 | 2410614  7168880 | 3051434   58187  6094545   104.7 |  0.786 % |
c |     87379 | 2410614  7168880 | 3356577   87379  9881553   113.1 |  0.786 % |
#### 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.93 0.98 0.93 2/54 30792
Raw data (stat): 30792 (runsolver) R 30791 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547807908 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0009 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 42064 0 0 0 900 99 0 0 25 0 1 0 547807908 176091136 37798 4294967295 134512640 134672761 3221224544 3221153920 1075349701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42991 37798 603 41 0 42950 0
vsize: 171964
[startup+20.0011 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75135 0 0 0 1820 179 0 0 25 0 1 0 547807908 322052096 70869 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78626 70869 603 41 0 78585 0
vsize: 314504
[startup+30.0017 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75211 0 0 0 2820 179 0 0 25 0 1 0 547807908 322457600 70945 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78725 70945 603 41 0 78684 0
vsize: 314900
[startup+40.0018 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75247 0 0 0 3819 180 0 0 25 0 1 0 547807908 322592768 70981 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78758 70981 603 41 0 78717 0
vsize: 315032
[startup+50.0021 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75712 0 0 0 4818 181 0 0 25 0 1 0 547807908 323678208 71446 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79023 71446 603 41 0 78982 0
vsize: 316092
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75814 0 0 0 5818 182 0 0 25 0 1 0 547807908 324083712 71548 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79122 71548 603 41 0 79081 0
vsize: 316488
[startup+70.0038 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75877 0 0 0 6817 182 0 0 25 0 1 0 547807908 324354048 71611 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79188 71611 603 41 0 79147 0
vsize: 316752
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75929 0 0 0 7817 183 0 0 25 0 1 0 547807908 324485120 71663 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79220 71663 603 41 0 79179 0
vsize: 316880
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 75984 0 0 0 8817 183 0 0 25 0 1 0 547807908 324755456 71718 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79286 71718 603 41 0 79245 0
vsize: 317144
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76052 0 0 0 9817 184 0 0 25 0 1 0 547807908 325021696 71786 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79351 71786 603 41 0 79310 0
vsize: 317404
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76144 0 0 0 10816 184 0 0 25 0 1 0 547807908 325419008 71878 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79448 71878 603 41 0 79407 0
vsize: 317792
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76223 0 0 0 11816 185 0 0 25 0 1 0 547807908 325685248 71957 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79513 71957 603 41 0 79472 0
vsize: 318052
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76290 0 0 0 12816 185 0 0 25 0 1 0 547807908 325951488 72024 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79578 72024 603 41 0 79537 0
vsize: 318312
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76358 0 0 0 13815 185 0 0 25 0 1 0 547807908 326348800 72092 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79675 72092 603 41 0 79634 0
vsize: 318700
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76423 0 0 0 14815 186 0 0 25 0 1 0 547807908 326615040 72157 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79740 72157 603 41 0 79699 0
vsize: 318960
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76508 0 0 0 15815 186 0 0 25 0 1 0 547807908 326885376 72242 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79806 72242 603 41 0 79765 0
vsize: 319224
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76578 0 0 0 16814 187 0 0 25 0 1 0 547807908 327208960 72312 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79885 72312 603 41 0 79844 0
vsize: 319540
[startup+180.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76619 0 0 0 17814 187 0 0 25 0 1 0 547807908 327340032 72353 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79917 72353 603 41 0 79876 0
vsize: 319668
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76668 0 0 0 18814 188 0 0 25 0 1 0 547807908 327659520 72402 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79995 72402 603 41 0 79954 0
vsize: 319980
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76706 0 0 0 19814 188 0 0 25 0 1 0 547807908 327794688 72440 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80028 72440 603 41 0 79987 0
vsize: 320112
[startup+210.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76747 0 0 0 20813 189 0 0 25 0 1 0 547807908 327929856 72481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80061 72481 603 41 0 80020 0
vsize: 320244
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76791 0 0 0 21813 189 0 0 25 0 1 0 547807908 328060928 72525 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80093 72525 603 41 0 80052 0
vsize: 320372
[startup+230.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76838 0 0 0 22814 189 0 0 25 0 1 0 547807908 328331264 72572 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80159 72572 603 41 0 80118 0
vsize: 320636
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76880 0 0 0 23813 189 0 0 25 0 1 0 547807908 328462336 72614 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80191 72614 603 41 0 80150 0
vsize: 320764
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30792
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76921 0 0 0 24813 189 0 0 25 0 1 0 547807908 328593408 72655 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80223 72655 603 41 0 80182 0
vsize: 320892
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 76966 0 0 0 25813 189 0 0 25 0 1 0 547807908 328863744 72700 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80289 72700 603 41 0 80248 0
vsize: 321156
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77008 0 0 0 26814 189 0 0 25 0 1 0 547807908 328998912 72742 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80322 72742 603 41 0 80281 0
vsize: 321288
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77053 0 0 0 27813 190 0 0 25 0 1 0 547807908 329134080 72787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80355 72787 603 41 0 80314 0
vsize: 321420
[startup+290.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77092 0 0 0 28814 190 0 0 25 0 1 0 547807908 329269248 72826 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80388 72826 603 41 0 80347 0
vsize: 321552
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77142 0 0 0 29813 190 0 0 25 0 1 0 547807908 329539584 72876 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80454 72876 603 41 0 80413 0
vsize: 321816
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77183 0 0 0 30813 191 0 0 25 0 1 0 547807908 329670656 72917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80486 72917 603 41 0 80445 0
vsize: 321944
[startup+320.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77220 0 0 0 31813 191 0 0 25 0 1 0 547807908 329801728 72954 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80518 72954 603 41 0 80477 0
vsize: 322072
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77440 0 0 0 32812 192 0 0 25 0 1 0 547807908 330747904 73174 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80749 73174 603 41 0 80708 0
vsize: 322996
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77648 0 0 0 33811 192 0 0 25 0 1 0 547807908 331558912 73382 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80947 73382 603 41 0 80906 0
vsize: 323788
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 77809 0 0 0 34811 193 0 0 25 0 1 0 547807908 332230656 73543 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81111 73543 603 41 0 81070 0
vsize: 324444
[startup+360.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78057 0 0 0 35810 194 0 0 25 0 1 0 547807908 333312000 73791 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81375 73791 603 41 0 81334 0
vsize: 325500
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78187 0 0 0 36810 194 0 0 25 0 1 0 547807908 333852672 73921 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81507 73921 603 41 0 81466 0
vsize: 326028
[startup+380.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78308 0 0 0 37810 194 0 0 25 0 1 0 547807908 334393344 74042 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81639 74042 603 41 0 81598 0
vsize: 326556
[startup+390.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78436 0 0 0 38809 195 0 0 25 0 1 0 547807908 334798848 74170 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81738 74170 603 41 0 81697 0
vsize: 326952
[startup+400.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78552 0 0 0 39809 195 0 0 25 0 1 0 547807908 335335424 74286 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81869 74286 603 41 0 81828 0
vsize: 327476
[startup+410.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78635 0 0 0 40809 195 0 0 25 0 1 0 547807908 335605760 74369 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81935 74369 603 41 0 81894 0
vsize: 327740
[startup+420.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78774 0 0 0 41809 196 0 0 25 0 1 0 547807908 336273408 74508 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82098 74508 603 41 0 82057 0
vsize: 328392
[startup+430.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78890 0 0 0 42809 196 0 0 25 0 1 0 547807908 336670720 74624 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82195 74624 603 41 0 82154 0
vsize: 328780
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 78978 0 0 0 43809 196 0 0 25 0 1 0 547807908 337072128 74712 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82293 74712 603 41 0 82252 0
vsize: 329172
[startup+450.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79046 0 0 0 44809 197 0 0 25 0 1 0 547807908 337338368 74780 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82358 74780 603 41 0 82317 0
vsize: 329432
[startup+460.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79106 0 0 0 45809 197 0 0 25 0 1 0 547807908 337608704 74840 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82424 74840 603 41 0 82383 0
vsize: 329696
[startup+470.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79239 0 0 0 46809 197 0 0 25 0 1 0 547807908 338149376 74973 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82556 74973 603 41 0 82515 0
vsize: 330224
[startup+480.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79350 0 0 0 47809 197 0 0 25 0 1 0 547807908 338554880 75084 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82655 75084 603 41 0 82614 0
vsize: 330620
[startup+490.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79461 0 0 0 48809 198 0 0 25 0 1 0 547807908 339087360 75195 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82785 75195 603 41 0 82744 0
vsize: 331140
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79565 0 0 0 49809 198 0 0 25 0 1 0 547807908 339484672 75299 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82882 75299 603 41 0 82841 0
vsize: 331528
[startup+510.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79666 0 0 0 50808 198 0 0 25 0 1 0 547807908 339881984 75400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82979 75400 603 41 0 82938 0
vsize: 331916
[startup+520.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79809 0 0 0 51808 199 0 0 25 0 1 0 547807908 340418560 75543 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83110 75543 603 41 0 83069 0
vsize: 332440
[startup+530.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 79915 0 0 0 52808 199 0 0 25 0 1 0 547807908 340959232 75649 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83242 75649 603 41 0 83201 0
vsize: 332968
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80017 0 0 0 53808 199 0 0 25 0 1 0 547807908 341364736 75751 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83341 75751 603 41 0 83300 0
vsize: 333364
[startup+550.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80133 0 0 0 54808 199 0 0 25 0 1 0 547807908 341774336 75867 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83441 75867 603 41 0 83400 0
vsize: 333764
[startup+560.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80217 0 0 0 55808 200 0 0 25 0 1 0 547807908 342175744 75951 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83539 75951 603 41 0 83498 0
vsize: 334156
[startup+570.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80322 0 0 0 56808 200 0 0 25 0 1 0 547807908 342577152 76056 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83637 76056 603 41 0 83596 0
vsize: 334548
[startup+580.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80412 0 0 0 57808 200 0 0 25 0 1 0 547807908 342974464 76146 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83734 76146 603 41 0 83693 0
vsize: 334936
[startup+590.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80468 0 0 0 58808 201 0 0 25 0 1 0 547807908 343105536 76202 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83766 76202 603 41 0 83725 0
vsize: 335064
[startup+600.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80533 0 0 0 59808 201 0 0 25 0 1 0 547807908 343367680 76267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83830 76267 603 41 0 83789 0
vsize: 335320
[startup+610.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80592 0 0 0 60808 201 0 0 25 0 1 0 547807908 343629824 76326 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83894 76326 603 41 0 83853 0
vsize: 335576
[startup+620.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80661 0 0 0 61808 201 0 0 25 0 1 0 547807908 343896064 76395 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83959 76395 603 41 0 83918 0
vsize: 335836
[startup+630.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80734 0 0 0 62808 201 0 0 25 0 1 0 547807908 344293376 76468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84056 76468 603 41 0 84015 0
vsize: 336224
[startup+640.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80789 0 0 0 63808 201 0 0 25 0 1 0 547807908 344424448 76523 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84088 76523 603 41 0 84047 0
vsize: 336352
[startup+650.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80845 0 0 0 64808 202 0 0 25 0 1 0 547807908 344817664 76579 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84184 76579 603 41 0 84143 0
vsize: 336736
[startup+660.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80901 0 0 0 65808 202 0 0 25 0 1 0 547807908 345083904 76635 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84249 76635 603 41 0 84208 0
vsize: 336996
[startup+670.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 80958 0 0 0 66808 202 0 0 25 0 1 0 547807908 345214976 76692 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84281 76692 603 41 0 84240 0
vsize: 337124
[startup+680.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81014 0 0 0 67808 202 0 0 25 0 1 0 547807908 345477120 76748 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84345 76748 603 41 0 84304 0
vsize: 337380
[startup+690.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81079 0 0 0 68808 202 0 0 25 0 1 0 547807908 345739264 76813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84409 76813 603 41 0 84368 0
vsize: 337636
[startup+700.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81149 0 0 0 69808 202 0 0 25 0 1 0 547807908 346025984 76883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84479 76883 603 41 0 84438 0
vsize: 337916
[startup+710.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81220 0 0 0 70808 203 0 0 25 0 1 0 547807908 346292224 76954 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84544 76954 603 41 0 84503 0
vsize: 338176
[startup+720.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81272 0 0 0 71808 203 0 0 25 0 1 0 547807908 346558464 77006 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84609 77006 603 41 0 84568 0
vsize: 338436
[startup+730.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81324 0 0 0 72808 203 0 0 25 0 1 0 547807908 346689536 77058 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84641 77058 603 41 0 84600 0
vsize: 338564
[startup+740.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81382 0 0 0 73808 204 0 0 25 0 1 0 547807908 346951680 77116 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84705 77116 603 41 0 84664 0
vsize: 338820
[startup+750.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81443 0 0 0 74808 204 0 0 25 0 1 0 547807908 347213824 77177 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84769 77177 603 41 0 84728 0
vsize: 339076
[startup+760.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81490 0 0 0 75808 204 0 0 25 0 1 0 547807908 347480064 77224 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84834 77224 603 41 0 84793 0
vsize: 339336
[startup+770.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81543 0 0 0 76808 204 0 0 25 0 1 0 547807908 347611136 77277 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84866 77277 603 41 0 84825 0
vsize: 339464
[startup+780.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81598 0 0 0 77808 204 0 0 25 0 1 0 547807908 347877376 77332 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84931 77332 603 41 0 84890 0
vsize: 339724
[startup+790.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81646 0 0 0 78808 204 0 0 25 0 1 0 547807908 348008448 77380 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84963 77380 603 41 0 84922 0
vsize: 339852
[startup+800.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81710 0 0 0 79808 204 0 0 25 0 1 0 547807908 348278784 77444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85029 77444 603 41 0 84988 0
vsize: 340116
[startup+810.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81766 0 0 0 80808 205 0 0 25 0 1 0 547807908 348549120 77500 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85095 77500 603 41 0 85054 0
vsize: 340380
[startup+820.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81813 0 0 0 81808 205 0 0 25 0 1 0 547807908 348680192 77547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85127 77547 603 41 0 85086 0
vsize: 340508
[startup+830.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81883 0 0 0 82809 205 0 0 25 0 1 0 547807908 349077504 77617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85224 77617 603 41 0 85183 0
vsize: 340896
[startup+840.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 81972 0 0 0 83810 205 0 0 25 0 1 0 547807908 349339648 77706 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85288 77706 603 41 0 85247 0
vsize: 341152
[startup+850.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82048 0 0 0 84810 205 0 0 25 0 1 0 547807908 349736960 77782 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85385 77782 603 41 0 85344 0
vsize: 341540
[startup+860.052 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82127 0 0 0 85811 205 0 0 25 0 1 0 547807908 349999104 77861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85449 77861 603 41 0 85408 0
vsize: 341796
[startup+870.067 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82186 0 0 0 86812 206 0 0 25 0 1 0 547807908 350261248 77920 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85513 77920 603 41 0 85472 0
vsize: 342052
[startup+880.067 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82256 0 0 0 87812 206 0 0 25 0 1 0 547807908 350531584 77990 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85579 77990 603 41 0 85538 0
vsize: 342316
[startup+890.068 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82355 0 0 0 88812 206 0 0 25 0 1 0 547807908 350937088 78089 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85678 78089 603 41 0 85637 0
vsize: 342712
[startup+900.067 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82466 0 0 0 89812 207 0 0 25 0 1 0 547807908 351334400 78200 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85775 78200 603 41 0 85734 0
vsize: 343100
[startup+910.076 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82556 0 0 0 90812 207 0 0 25 0 1 0 547807908 351735808 78290 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85873 78290 603 41 0 85832 0
vsize: 343492
[startup+920.076 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82634 0 0 0 91812 208 0 0 25 0 1 0 547807908 352006144 78368 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85939 78368 603 41 0 85898 0
vsize: 343756
[startup+930.075 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82711 0 0 0 92811 208 0 0 25 0 1 0 547807908 352399360 78445 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86035 78445 603 41 0 85994 0
vsize: 344140
[startup+940.076 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82764 0 0 0 93812 208 0 0 25 0 1 0 547807908 352534528 78498 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86068 78498 603 41 0 86027 0
vsize: 344272
[startup+950.076 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82831 0 0 0 94811 209 0 0 25 0 1 0 547807908 352800768 78565 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86133 78565 603 41 0 86092 0
vsize: 344532
[startup+960.075 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82902 0 0 0 95811 209 0 0 25 0 1 0 547807908 353202176 78636 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86231 78636 603 41 0 86190 0
vsize: 344924
[startup+970.075 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 82988 0 0 0 96811 209 0 0 25 0 1 0 547807908 353468416 78722 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86296 78722 603 41 0 86255 0
vsize: 345184
[startup+980.075 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83069 0 0 0 97811 209 0 0 25 0 1 0 547807908 353865728 78803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86393 78803 603 41 0 86352 0
vsize: 345572
[startup+990.074 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83142 0 0 0 98811 209 0 0 25 0 1 0 547807908 354136064 78876 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86459 78876 603 41 0 86418 0
vsize: 345836
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83221 0 0 0 99811 210 0 0 25 0 1 0 547807908 354668544 78955 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86589 78955 603 41 0 86548 0
vsize: 346356
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83311 0 0 0 100811 210 0 0 25 0 1 0 547807908 355069952 79045 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86687 79045 603 41 0 86646 0
vsize: 346748
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83482 0 0 0 101811 211 0 0 25 0 1 0 547807908 355741696 79216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86851 79216 603 41 0 86810 0
vsize: 347404
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83681 0 0 0 102810 211 0 0 25 0 1 0 547807908 356544512 79415 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87047 79415 603 41 0 87006 0
vsize: 348188
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 83793 0 0 0 103810 212 0 0 25 0 1 0 547807908 357081088 79527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87178 79527 603 41 0 87137 0
vsize: 348712
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84162 0 0 0 104809 213 0 0 25 0 1 0 547807908 358563840 79896 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87540 79896 603 41 0 87499 0
vsize: 350160
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84524 0 0 0 105808 214 0 0 25 0 1 0 547807908 360042496 80258 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87901 80258 603 41 0 87860 0
vsize: 351604
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 84873 0 0 0 106807 215 0 0 25 0 1 0 547807908 361385984 80607 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88229 80607 603 41 0 88188 0
vsize: 352916
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85127 0 0 0 107807 216 0 0 25 0 1 0 547807908 362459136 80861 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88491 80861 603 41 0 88450 0
vsize: 353964
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85392 0 0 0 108806 217 0 0 25 0 1 0 547807908 363540480 81126 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88755 81126 603 41 0 88714 0
vsize: 355020
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 85680 0 0 0 109805 218 0 0 25 0 1 0 547807908 364773376 81414 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89056 81414 603 41 0 89015 0
vsize: 356224
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86050 0 0 0 110803 219 0 0 25 0 1 0 547807908 366272512 81784 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89422 81784 603 41 0 89381 0
vsize: 357688
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86334 0 0 0 111802 220 0 0 25 0 1 0 547807908 367484928 82068 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89718 82068 603 41 0 89677 0
vsize: 358872
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86498 0 0 0 112801 221 0 0 25 0 1 0 547807908 368160768 82232 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89883 82232 603 41 0 89842 0
vsize: 359532
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86618 0 0 0 113800 222 0 0 25 0 1 0 547807908 368562176 82352 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89981 82352 603 41 0 89940 0
vsize: 359924
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86726 0 0 0 114799 223 0 0 25 0 1 0 547807908 369102848 82460 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90113 82460 603 41 0 90072 0
vsize: 360452
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86820 0 0 0 115799 223 0 0 25 0 1 0 547807908 369373184 82554 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90179 82554 603 41 0 90138 0
vsize: 360716
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86873 0 0 0 116799 223 0 0 25 0 1 0 547807908 369643520 82607 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90245 82607 603 41 0 90204 0
vsize: 360980
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86917 0 0 0 117799 223 0 0 25 0 1 0 547807908 369778688 82651 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90278 82651 603 41 0 90237 0
vsize: 361112
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 86970 0 0 0 118799 223 0 0 25 0 1 0 547807908 370049024 82704 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90344 82704 603 41 0 90303 0
vsize: 361376
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 30794
Raw data (stat): 30792 (minisat+) R 30791 10614 10613 0 -1 0 87039 0 0 0 119799 224 0 0 25 0 1 0 547807908 370319360 82773 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90410 82773 603 41 0 90369 0
vsize: 361640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 30794
Raw data (stat): 30792 (minisat+) Z 30791 10614 10613 0 -1 12 87041 0 0 0 119799 240 0 0 25 0 1 0 547807908 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.4
CPU user time (s): 1197.99
CPU system time (s): 2.40363
CPU usage (%): 100.013
Max. virtual memory (Kb): 361640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####