PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

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

General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-fiber.opb
MD5SUM	d1d488615de0d5a5bcf2a298507e66b1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	108097879
Optimality of the best value was proved	NO
Number of terms in the objective function	1254
Biggest coefficient in the objective function	72966962
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	4807778524
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	72966962
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	4807778524
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	90.9232
Number of variables	2134
Total number of constraints	1617
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1290
Number of constraints which are nor clauses,nor cardinality constraints	327
Minimum length of a constraint	1
Maximum length of a constraint	51

Trace number 18707

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 16:24:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17537 boxname=wulflinc12 idbench=1349 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d1d488615de0d5a5bcf2a298507e66b1  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fiber.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fiber.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-fiber.opb
IDLAUNCH: 17537
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        775320 kB
Buffers:         26856 kB
Cached:         211112 kB
SwapCached:        508 kB
Active:          52776 kB
Inactive:       187328 kB
HighTotal:      131008 kB
HighFree:        31556 kB
LowTotal:       903652 kB
LowFree:        743764 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13540 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:25:33 (client local time) WITH STATUS 1 IN 57.7772 SECONDS
stats: 17537 7 57.7772 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 696 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 694]---> Sorter-cost: 1575     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 692]---> Adder-cost: 148   maxlim: 187647   bits: 19/18
c ---[ 690]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    3
c ---[ 686]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:   13
c ---[ 682]---> BDD-cost:   17
c ---[ 680]---> BDD-cost:   13
c ---[ 678]---> BDD-cost:    9
c ---[ 676]---> BDD-cost:    5
c ---[ 674]---> BDD-cost:   30
c ---[ 672]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 670]---> BDD-cost:    6
c ---[ 668]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   21
c ---[ 664]---> BDD-cost:    6
c ---[ 662]---> BDD-cost:    6
c ---[ 660]---> BDD-cost:    6
c ---[ 658]---> BDD-cost:    6
c ---[ 656]---> BDD-cost:    6
c ---[ 654]---> BDD-cost:   13
c ---[ 652]---> BDD-cost:    1
c ---[ 650]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> BDD-cost:    6
c ---[ 646]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   17
c ---[ 642]---> BDD-cost:   22
c ---[ 640]---> BDD-cost:   22
c ---[ 638]---> BDD-cost:    0
c ---[ 636]---> BDD-cost:   13
c ---[ 634]---> BDD-cost:    1
c ---[ 632]---> BDD-cost:    1
c ---[ 630]---> BDD-cost:    1
c ---[ 628]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 626]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   14
c ---[ 622]---> BDD-cost:   13
c ---[ 620]---> BDD-cost:    9
c ---[ 618]---> BDD-cost:    5
c ---[ 616]---> BDD-cost:   30
c ---[ 614]---> BDD-cost:    6
c ---[ 612]---> BDD-cost:   13
c ---[ 610]---> BDD-cost:   16
c ---[ 608]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 606]---> BDD-cost:    6
c ---[ 604]---> BDD-cost:    9
c ---[ 602]---> BDD-cost:    6
c ---[ 600]---> BDD-cost:    6
c ---[ 598]---> BDD-cost:    6
c ---[ 596]---> BDD-cost:   13
c ---[ 594]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    9
c ---[ 590]---> BDD-cost:   17
c ---[ 588]---> BDD-cost:   17
c ---[ 586]---> Adder-cost: 148   maxlim: 189695   bits: 19/18
c ---[ 584]---> BDD-cost:   17
c ---[ 582]---> BDD-cost:   27
c ---[ 580]---> BDD-cost:   22
c ---[ 578]---> BDD-cost:   13
c ---[ 576]---> BDD-cost:    1
c ---[ 574]---> BDD-cost:    1
c ---[ 572]---> BDD-cost:    1
c ---[ 570]---> BDD-cost:   13
c ---[ 568]---> BDD-cost:   14
c ---[ 566]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 564]---> BDD-cost:   13
c ---[ 562]---> BDD-cost:    9
c ---[ 560]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:   30
c ---[ 556]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:   13
c ---[ 552]---> BDD-cost:   21
c ---[ 550]---> BDD-cost:    6
c ---[ 548]---> BDD-cost:    9
c ---[ 546]---> BDD-cost:    6
c ---[ 544]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 542]---> BDD-cost:    6
c ---[ 540]---> BDD-cost:    6
c ---[ 538]---> BDD-cost:   13
c ---[ 536]---> BDD-cost:    1
c ---[ 534]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:   17
c ---[ 530]---> BDD-cost:   17
c ---[ 528]---> BDD-cost:   27
c ---[ 526]---> BDD-cost:   27
c ---[ 524]---> BDD-cost:   22
c ---[ 522]---> Adder-cost: 148   maxlim: 182783   bits: 19/18
c ---[ 520]---> BDD-cost:    0
c ---[ 518]---> BDD-cost:   13
c ---[ 516]---> BDD-cost:    1
c ---[ 514]---> BDD-cost:    1
c ---[ 512]---> BDD-cost:    1
c ---[ 510]---> BDD-cost:   14
c ---[ 508]---> BDD-cost:   13
c ---[ 506]---> BDD-cost:    9
c ---[ 504]---> BDD-cost:    5
c ---[ 502]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 500]---> BDD-cost:   27
c ---[ 498]---> BDD-cost:    6
c ---[ 496]---> BDD-cost:   13
c ---[ 494]---> BDD-cost:   21
c ---[ 492]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    9
c ---[ 488]---> BDD-cost:    6
c ---[ 486]---> BDD-cost:    6
c ---[ 484]---> BDD-cost:    3
c ---[ 482]---> BDD-cost:    9
c ---[ 480]---> Adder-cost: 148   maxlim: 189183   bits: 19/18
c ---[ 478]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 476]---> BDD-cost:    1
c ---[ 474]---> BDD-cost:    9
c ---[ 472]---> BDD-cost:   17
c ---[ 470]---> BDD-cost:   17
c ---[ 468]---> BDD-cost:   27
c ---[ 466]---> BDD-cost:   27
c ---[ 464]---> BDD-cost:   22
c ---[ 462]---> BDD-cost:    0
c ---[ 460]---> BDD-cost:    9
c ---[ 458]---> BDD-cost:    1
c ---[ 456]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 454]---> BDD-cost:    1
c ---[ 452]---> BDD-cost:    1
c ---[ 450]---> BDD-cost:   13
c ---[ 448]---> BDD-cost:   13
c ---[ 446]---> BDD-cost:    6
c ---[ 444]---> BDD-cost:    5
c ---[ 442]---> BDD-cost:   24
c ---[ 440]---> BDD-cost:    6
c ---[ 438]---> BDD-cost:   13
c ---[ 436]---> Sorter-cost: 1002     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 434]---> BDD-cost:   21
c ---[ 432]---> BDD-cost:    6
c ---[ 430]---> BDD-cost:    9
c ---[ 428]---> BDD-cost:    6
c ---[ 426]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:    6
c ---[ 422]---> BDD-cost:   13
c ---[ 420]---> BDD-cost:    1
c ---[ 418]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:   13
c ---[ 414]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 412]---> BDD-cost:   17
c ---[ 410]---> BDD-cost:   27
c ---[ 408]---> BDD-cost:   27
c ---[ 406]---> BDD-cost:   22
c ---[ 404]---> BDD-cost:    0
c ---[ 402]---> BDD-cost:   13
c ---[ 400]---> BDD-cost:    1
c ---[ 398]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:    1
c ---[ 394]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 392]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:   10
c ---[ 388]---> BDD-cost:   13
c ---[ 386]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    5
c ---[ 382]---> BDD-cost:    6
c ---[ 380]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:   21
c ---[ 376]---> BDD-cost:    3
c ---[ 374]---> BDD-cost:    9
c ---[ 372]---> Adder-cost: 148   maxlim: 183039   bits: 19/18
c ---[ 370]---> BDD-cost:    6
c ---[ 368]---> BDD-cost:    6
c ---[ 366]---> BDD-cost:    6
c ---[ 364]---> BDD-cost:   13
c ---[ 362]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:   17
c ---[ 356]---> BDD-cost:   17
c ---[ 354]---> BDD-cost:   27
c ---[ 352]---> BDD-cost:   27
c ---[ 350]---> Adder-cost: 148   maxlim: 189183   bits: 19/18
c ---[ 348]---> BDD-cost:   22
c ---[ 346]---> BDD-cost:    0
c ---[ 344]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    1
c ---[ 340]---> BDD-cost:    1
c ---[ 338]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:   13
c ---[ 334]---> BDD-cost:   14
c ---[ 332]---> BDD-cost:   13
c ---[ 330]---> Adder-cost: 148   maxlim: 196607   bits: 19/18
c ---[ 328]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    5
c ---[ 324]---> BDD-cost:   24
c ---[ 322]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:   21
c ---[ 318]---> BDD-cost:    6
c ---[ 316]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    6
c ---[ 312]---> BDD-cost:    6
c ---[ 310]---> BDD-cost:    6
c ---[ 308]---> Adder-cost: 148   maxlim: 198783   bits: 19/18
c ---[ 306]---> BDD-cost:   13
c ---[ 304]---> BDD-cost:    1
c ---[ 302]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:   17
c ---[ 298]---> BDD-cost:   17
c ---[ 296]---> BDD-cost:   22
c ---[ 294]---> BDD-cost:   27
c ---[ 292]---> BDD-cost:   17
c ---[ 290]---> BDD-cost:    0
c ---[ 288]---> BDD-cost:   13
c ---[ 286]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 284]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   14
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    5
c ---[ 270]---> BDD-cost:   30
c ---[ 268]---> Adder-cost: 148   maxlim: 195199   bits: 19/18
c ---[ 266]---> Adder-cost: 148   maxlim: 199167   bits: 19/18
c ---[ 264]---> BDD-cost:    6
c ---[ 262]---> BDD-cost:   13
c ---[ 260]---> BDD-cost:    6
c ---[ 258]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:    6
c ---[ 250]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:    9
c ---[ 246]---> Adder-cost: 148   maxlim: 182271   bits: 19/18
c ---[ 244]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   27
c ---[ 238]---> BDD-cost:   27
c ---[ 236]---> BDD-cost:   22
c ---[ 234]---> BDD-cost:    0
c ---[ 232]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 226]---> BDD-cost:    1
c ---[ 224]---> Adder-cost: 148   maxlim: 166527   bits: 19/18
c ---[ 222]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:   14
c ---[ 218]---> BDD-cost:   13
c ---[ 216]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:   30
c ---[ 210]---> BDD-cost:    6
c ---[ 208]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   21
c ---[ 204]---> Adder-cost: 148   maxlim: 197887   bits: 19/18
c ---[ 202]---> BDD-cost:    6
c ---[ 200]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    6
c ---[ 196]---> BDD-cost:    6
c ---[ 194]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    1
c ---[ 190]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   27
c ---[ 182]---> Adder-cost: 148   maxlim: 198399   bits: 19/18
c ---[ 180]---> BDD-cost:   22
c ---[ 178]---> BDD-cost:   22
c ---[ 176]---> BDD-cost:    0
c ---[ 174]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   14
c ---[ 162]---> Adder-cost: 148   maxlim: 181503   bits: 19/18
c ---[ 160]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:   30
c ---[ 152]---> BDD-cost:    6
c ---[ 150]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    6
c ---[ 142]---> BDD-cost:    6
c ---[ 140]---> Adder-cost: 148   maxlim: 181247   bits: 19/18
c ---[ 138]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:   13
c ---[ 132]---> BDD-cost:    1
c ---[ 130]---> Adder-cost: 148   maxlim: 194559   bits: 19/18
c ---[ 128]---> Adder-cost: 148   maxlim: 195199   bits: 19/18
c ---[ 126]---> Sorter-cost: 1657     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 124]---> Adder-cost: 148   maxlim: 197375   bits: 19/18
c ---[ 122]---> Adder-cost: 148   maxlim: 196863   bits: 19/18
c ---[ 120]---> Adder-cost: 148   maxlim: 198911   bits: 19/18
c ---[ 118]---> Adder-cost: 148   maxlim: 198399   bits: 19/18
c ---[ 116]---> Adder-cost: 148   maxlim: 196479   bits: 19/18
c ---[ 114]---> Adder-cost: 148   maxlim: 196607   bits: 19/18
c ---[ 112]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:    7
c ---[ 108]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:    3
c ---[ 104]---> Adder-cost: 148   maxlim: 181119   bits: 19/18
c ---[ 102]---> BDD-cost:    5
c ---[ 100]---> BDD-cost:    7
c ---[  98]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    3
c ---[  90]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   15
c ---[  84]---> BDD-cost:   15
c ---[  82]---> Adder-cost: 148   maxlim: 193407   bits: 19/18
c ---[  80]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   22
c ---[  60]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[  58]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   13
c ---[  54]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  48]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  42]---> Sorter-cost: 1657     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[  40]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    5
c ---[  36]---> BDD-cost:   30
c ---[  34]---> BDD-cost:    6
c ---[  32]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   16
c ---[  28]---> BDD-cost:    6
c ---[  26]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    6
c ---[  22]---> BDD-cost:    6
c ---[  20]---> Sorter-cost: 1004     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:   13
c ---[  14]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   22
c ---[   4]---> BDD-cost:   17
c ---[   2]---> BDD-cost:    0
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80240   231728 |   26746       0        0     nan |  0.000 % |
c |       100 |   80236   231718 |   29420      99      999    10.1 | 10.297 % |
c |       251 |   80236   231718 |   32362     250     1947     7.8 | 10.297 % |
c |       477 |   80225   231687 |   35598     472     3647     7.7 | 10.305 % |
c |       814 |   80173   231545 |   39158     805     6255     7.8 | 10.363 % |
c |      1320 |   80173   231545 |   43074    1311    10562     8.1 | 10.363 % |
c |      2079 |   80149   231479 |   47382    2066    15890     7.7 | 10.385 % |
c |      3218 |   80068   231252 |   52120    3193    25083     7.9 | 10.455 % |
c |      4928 |   79997   231041 |   57332    4897    42064     8.6 | 10.512 % |
c |      7490 |   79814   230551 |   63065    7442    64600     8.7 | 10.692 % |
c |     11334 |   79768   230426 |   69372   11275   101553     9.0 | 10.736 % |
c |     17100 |   79267   229139 |   76309   16980   159663     9.4 | 11.233 % |
c |     25749 |   78658   227565 |   83940   25529   253193     9.9 | 11.830 % |
c |     38723 |   78126   226104 |   92334   38390   390959    10.2 | 12.331 % |
c |     58184 |   77585   224658 |  101567   57772   626237    10.8 | 12.868 % |
ERROR! Too large constants encountered in constraint.
c ==============================================================================
c [1mFound solution: -1864975952[0m
#### 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.92 2/54 31762
Raw data (stat): 31762 (runsolver) R 31761 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488273152 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.81 0.93 0.92 2/54 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 2665 0 0 0 992 6 0 0 25 0 1 0 488273152 12922880 2588 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2588 603 41 0 3114 0
vsize: 12620
[startup+20.0002 s]
Raw data (loadavg): 0.84 0.93 0.92 2/54 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 2861 0 0 0 1991 6 0 0 25 0 1 0 488273152 13729792 2784 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2784 603 41 0 3311 0
vsize: 13408
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.93 0.92 2/54 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 3021 0 0 0 2991 7 0 0 25 0 1 0 488273152 14397440 2944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3515 2944 603 41 0 3474 0
vsize: 14060
[startup+40.0008 s]
Raw data (loadavg): 0.89 0.93 0.92 2/54 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 3214 0 0 0 3990 7 0 0 25 0 1 0 488273152 15196160 3137 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3710 3137 603 41 0 3669 0
vsize: 14840
[startup+50.0017 s]
Raw data (loadavg): 0.90 0.93 0.92 2/54 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 3479 0 0 0 4990 8 0 0 25 0 1 0 488273152 16269312 3402 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3972 3402 603 41 0 3931 0
vsize: 15888
[startup+57.7965 s]
Raw data (loadavg): 0.92 0.93 0.92 1/53 31762
Raw data (stat): 31762 (minisat+) R 31761 25285 25284 0 -1 0 3479 0 0 0 4990 8 0 0 25 0 1 0 488273152 16269312 3402 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3972 3402 603 41 0 3931 0
vsize: 0

Child status: 1
Real time (s): 57.7962
CPU time (s): 57.7772
CPU user time (s): 57.6782
CPU system time (s): 0.098984
CPU usage (%): 99.9672
Max. virtual memory (Kb): 15888
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####