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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM	6049145b9f1adfd7114adf044503d587
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2642
Optimality of the best value was proved	NO
Number of terms in the objective function	748
Biggest coefficient in the objective function	240
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	33855
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	240
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	33855
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	907
Total number of constraints	1309
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	1183
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	134
Trace number 31733

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-27 05:56:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23112 boxname=wulflinc18 idbench=358 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc18/normalized-ws97-5.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-ws97-5.opb
IDLAUNCH: 23112
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        633504 kB
Buffers:         39156 kB
Cached:         333848 kB
SwapCached:        588 kB
Active:          73548 kB
Inactive:       304864 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        633252 kB
SwapTotal:     2097892 kB
SwapFree:      2096632 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            17096 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 06:16:49 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 23112 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> BDD-cost: 3184
c ---[ 659]---> BDD-cost: 3184
c ---[ 658]---> BDD-cost: 3184
c ---[ 657]---> BDD-cost: 3127
c ---[ 656]---> BDD-cost: 4127
c ---[ 655]---> BDD-cost: 4164
c ---[ 654]---> BDD-cost: 4164
c ---[ 653]---> BDD-cost:  264
c ---[ 652]---> BDD-cost:  264
c ---[ 651]---> BDD-cost:  264
c ---[ 650]---> BDD-cost:  253
c ---[ 649]---> BDD-cost:  476
c ---[ 648]---> BDD-cost:  490
c ---[ 647]---> BDD-cost:  490
c ---[ 645]---> BDD-cost:    5
c ---[ 643]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    5
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    5
c ---[ 635]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    5
c ---[ 631]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    5
c ---[ 627]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    5
c ---[ 623]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    5
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    5
c ---[ 599]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    5
c ---[ 595]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    5
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    5
c ---[ 587]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    5
c ---[ 349]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    5
c ---[ 345]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    5
c ---[ 337]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 305]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    5
c ---[ 301]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 297]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    5
c ---[ 293]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    5
c ---[ 289]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 231]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    5
c ---[ 215]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    5
c ---[ 207]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    5
c ---[ 195]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    5
c ---[ 159]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    5
c ---[ 143]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    5
c ---[ 139]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    5
c ---[ 131]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  135304   403409 |   45101       0        0     nan |  0.000 % |
c |       100 |  135304   403409 |   49611     100     9086    90.9 |  0.947 % |
c ==============================================================================
c [1mFound solution: 4956[0m
c ---[   0]---> Sorter-cost:30425     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       135 |  198671   551567 |   66223     135     9297    68.9 |  0.947 % |
c |       235 |  198560   551316 |   72845     234    10391    44.4 |  0.560 % |
c |       385 |  195114   543424 |   80129     316    10681    33.8 |  2.414 % |
c |       610 |  190417   532586 |   88142     438    11126    25.4 |  5.064 % |
c |       955 |  185411   520991 |   96957     688    17050    24.8 |  7.954 % |
c |      1461 |  181632   512256 |  106652    1095    19319    17.6 | 10.127 % |
c |      2220 |  180253   509062 |  117318    1796    45024    25.1 | 10.923 % |
c |      3359 |  180241   509035 |  129049    2933    56845    19.4 | 10.929 % |
c |      5067 |  178333   504610 |  141954    4565   103112    22.6 | 12.048 % |
c |      7629 |  178333   504610 |  156150    7127   156417    21.9 | 12.048 % |
c |     11473 |  178305   504546 |  171765   10962   346002    31.6 | 12.062 % |
c |     17243 |  177011   501549 |  188941   16647   449140    27.0 | 12.819 % |
c |     25892 |  176265   499806 |  207836   25219   750685    29.8 | 13.279 % |
c |     38868 |  176201   499660 |  228619   38190  1196362    31.3 | 13.316 % |
c |     58329 |  176197   499651 |  251481   57649  2304801    40.0 | 13.317 % |
c ==============================================================================
c [1mFound solution: 4685[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63639 |  176609   500718 |   58869   62959  2947135    46.8 | 13.317 % |
c |     63741 |  176609   500718 |   64755   63061  2953100    46.8 | 13.543 % |
c |     63894 |  176609   500718 |   71231   63214  2961567    46.8 | 13.543 % |
c |     64120 |  176609   500718 |   78354   63440  2975855    46.9 | 13.543 % |
c |     64457 |  176609   500718 |   86190   63777  2986754    46.8 | 13.543 % |
c |     64963 |  176587   500668 |   94809   64282  3011376    46.8 | 13.554 % |
c |     65727 |  176587   500668 |  104290   65046  3077440    47.3 | 13.554 % |
c |     66866 |  176587   500668 |  114719   66185  3122708    47.2 | 13.554 % |
c |     68574 |  176587   500668 |  126190   67893  3201834    47.2 | 13.554 % |
c ==============================================================================
c [1mFound solution: 4470[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70270 |  176554   500600 |   58851   69588  3274794    47.1 | 13.554 % |
c |     70370 |  176554   500600 |   64736   17480   989767    56.6 | 13.634 % |
c |     70520 |  176554   500600 |   71209   17630   995638    56.5 | 13.634 % |
c |     70746 |  176554   500600 |   78330   17856  1000217    56.0 | 13.634 % |
c ==============================================================================
c [1mFound solution: 4256[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70795 |  176579   500666 |   58859   17905  1000629    55.9 | 13.634 % |
c |     70895 |  176579   500666 |   64744   18005  1005325    55.8 | 13.632 % |
c |     71046 |  176579   500666 |   71219   18156  1010044    55.6 | 13.632 % |
c |     71275 |  176522   500534 |   78341   18382  1012981    55.1 | 13.666 % |
c |     71613 |  176522   500534 |   86175   18720  1015432    54.2 | 13.666 % |
c |     72120 |  176522   500534 |   94793   19227  1030428    53.6 | 13.666 % |
c ==============================================================================
c [1mFound solution: 3855[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72759 |  176565   500649 |   58855   19866  1045801    52.6 | 13.666 % |
c |     72859 |  176565   500649 |   64740   19966  1050025    52.6 | 13.661 % |
c |     73009 |  176565   500649 |   71214   20116  1054667    52.4 | 13.661 % |
c |     73234 |  176565   500649 |   78336   20341  1068788    52.5 | 13.661 % |
c |     73574 |  176565   500649 |   86169   20681  1079331    52.2 | 13.661 % |
c |     74080 |  176565   500649 |   94786   21187  1110656    52.4 | 13.661 % |
c |     74839 |  176565   500649 |  104265   21946  1151114    52.5 | 13.661 % |
c ==============================================================================
c [1mFound solution: 3758[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75041 |  176920   501512 |   58973   22148  1160787    52.4 | 13.661 % |
c |     75143 |  176920   501512 |   64870   22250  1166820    52.4 | 13.869 % |
c |     75293 |  176920   501512 |   71357   22400  1170760    52.3 | 13.869 % |
c |     75518 |  176920   501512 |   78493   22625  1179462    52.1 | 13.869 % |
c |     75855 |  176920   501512 |   86342   22962  1195236    52.1 | 13.869 % |
c |     76362 |  176920   501512 |   94976   23469  1228074    52.3 | 13.869 % |
c ==============================================================================
c [1mFound solution: 3557[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76534 |  177139   502047 |   59046   23641  1236168    52.3 | 13.869 % |
c |     76637 |  177139   502047 |   64950   23744  1242033    52.3 | 13.988 % |
c |     76790 |  177139   502047 |   71445   23897  1248477    52.2 | 13.988 % |
c |     77016 |  177139   502047 |   78590   24123  1260565    52.3 | 13.988 % |
c ==============================================================================
c [1mFound solution: 3456[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77203 |  177159   502101 |   59053   24310  1267226    52.1 | 13.988 % |
c |     77303 |  177159   502101 |   64958   24410  1268190    52.0 | 13.987 % |
c |     77454 |  177159   502101 |   71454   24561  1269326    51.7 | 13.987 % |
c |     77680 |  177159   502101 |   78599   24787  1270540    51.3 | 13.987 % |
c |     78018 |  177159   502101 |   86459   25125  1284282    51.1 | 13.987 % |
c |     78524 |  177159   502101 |   95105   25631  1301635    50.8 | 13.987 % |
c |     79287 |  177159   502101 |  104615   26394  1355111    51.3 | 13.987 % |
c |     80428 |  177159   502101 |  115077   27535  1465511    53.2 | 13.987 % |
c ==============================================================================
c [1mFound solution: 3356[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81724 |  177166   502121 |   59055   28831  1532524    53.2 | 13.987 % |
c |     81824 |  177166   502121 |   64960   28931  1533887    53.0 | 13.988 % |
c |     81975 |  177166   502121 |   71456   29082  1539186    52.9 | 13.988 % |
c |     82204 |  177166   502121 |   78602   29311  1547487    52.8 | 13.988 % |
c |     82541 |  177166   502121 |   86462   29648  1566787    52.8 | 13.988 % |
c |     83050 |  177166   502121 |   95108   30157  1587318    52.6 | 13.988 % |
c |     83810 |  177166   502121 |  104619   30917  1664294    53.8 | 13.988 % |
c ==============================================================================
c [1mFound solution: 3351[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83955 |  177172   502135 |   59057   31062  1672532    53.8 | 13.988 % |
c |     84055 |  177172   502135 |   64962   31162  1678961    53.9 | 13.989 % |
c |     84205 |  177172   502135 |   71458   31312  1688008    53.9 | 13.989 % |
c |     84431 |  177172   502135 |   78604   31538  1701338    53.9 | 13.989 % |
c |     84770 |  177172   502135 |   86465   31877  1722913    54.0 | 13.989 % |
c |     85276 |  177172   502135 |   95111   32383  1746752    53.9 | 13.989 % |
c |     86035 |  177172   502135 |  104623   33142  1787689    53.9 | 13.989 % |
c |     87175 |  177172   502135 |  115085   34282  1865456    54.4 | 13.989 % |
c |     88883 |  177172   502135 |  126593   35990  1948262    54.1 | 13.989 % |
c |     91445 |  177172   502135 |  139253   38552  1999355    51.9 | 13.989 % |
c |     95293 |  177172   502135 |  153178   42400  2287146    53.9 | 13.989 % |
c |    101059 |  177172   502135 |  168496   48166  2626198    54.5 | 13.989 % |
c |    109708 |  177172   502135 |  185346   56815  3294504    58.0 | 13.989 % |
c |    122683 |  177166   502121 |  203880   69788  4387015    62.9 | 13.992 % |
c |    142145 |  177166   502121 |  224268   89250  5041971    56.5 | 13.992 % |
c ==============================================================================
c [1mFound solution: 3350[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    147746 |  177174   502139 |   59058   94851  5603739    59.1 | 13.992 % |
c |    147848 |  177174   502139 |   64963   19109   827494    43.3 | 13.993 % |
c |    147999 |  177174   502139 |   71460   19260   834771    43.3 | 13.993 % |
c |    148225 |  177174   502139 |   78606   19486   848989    43.6 | 13.993 % |
c |    148562 |  177174   502139 |   86466   19823   858209    43.3 | 13.993 % |
c |    149068 |  177170   502130 |   95113   20327   869523    42.8 | 13.995 % |
c |    149827 |  177170   502130 |  104624   21086   899825    42.7 | 13.995 % |
c |    150967 |  177170   502130 |  115087   22226   978243    44.0 | 13.995 % |
c |    152675 |  177170   502130 |  126596   23934  1077496    45.0 | 13.995 % |
c |    155237 |  177170   502130 |  139255   26496  1291780    48.8 | 13.995 % |
c |    159082 |  177170   502130 |  153181   30341  1425428    47.0 | 13.995 % |
c |    164850 |  177170   502130 |  168499   36109  1931271    53.5 | 13.995 % |
c |    173503 |  177170   502130 |  185349   44762  2818801    63.0 | 13.995 % |
c |    186477 |  177170   502130 |  203884   57736  4461250    77.3 | 13.995 % |
c |    205938 |  177170   502130 |  224272   77197  6193139    80.2 | 13.995 % |
c |    235130 |  177170   502130 |  246699  106389  7746072    72.8 | 13.995 % |
c ==============================================================================
c [1mFound solution: 3349[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239889 |  177376   502633 |   59125  111148  8274339    74.4 | 13.995 % |
c |    239990 |  177376   502633 |   65037   21629  1055139    48.8 | 14.110 % |
c |    240140 |  177376   502633 |   71541   21779  1065392    48.9 | 14.110 % |
c |    240366 |  177376   502633 |   78695   22005  1075377    48.9 | 14.110 % |
c |    240703 |  177376   502633 |   86564   22342  1093745    49.0 | 14.110 % |
c |    241209 |  177376   502633 |   95221   22848  1122300    49.1 | 14.110 % |
c |    241968 |  177376   502633 |  104743   23607  1181256    50.0 | 14.110 % |
c |    243107 |  177376   502633 |  115217   24746  1274774    51.5 | 14.110 % |
c ==============================================================================
c [1mFound solution: 3348[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    244188 |  177384   502651 |   59128   25827  1368244    53.0 | 14.110 % |
c |    244289 |  177384   502651 |   65040   25928  1370512    52.9 | 14.111 % |
c |    244439 |  177384   502651 |   71544   26078  1373093    52.7 | 14.111 % |
c |    244666 |  177384   502651 |   78699   26305  1397230    53.1 | 14.111 % |
c |    245003 |  177384   502651 |   86569   26642  1406176    52.8 | 14.111 % |
c |    245509 |  177384   502651 |   95226   27148  1466628    54.0 | 14.111 % |
c |    246268 |  177384   502651 |  104748   27907  1491851    53.5 | 14.111 % |
c |    247407 |  177384   502651 |  115223   29046  1546327    53.2 | 14.111 % |
c |    249115 |  177384   502651 |  126746   30754  1668825    54.3 | 14.111 % |
c |    251677 |  177384   502651 |  139420   33316  1805037    54.2 | 14.111 % |
c |    255522 |  177384   502651 |  153362   37161  2030785    54.6 | 14.111 % |
c ==============================================================================
c [1mFound solution: 3347[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    257747 |  177392   502669 |   59130   39386  2180548    55.4 | 14.111 % |
c |    257848 |  177392   502669 |   65043   39487  2184038    55.3 | 14.112 % |
c |    257999 |  177392   502669 |   71547   39638  2193084    55.3 | 14.112 % |
c |    258225 |  177392   502669 |   78702   39864  2197781    55.1 | 14.112 % |
c |    258562 |  177392   502669 |   86572   40201  2240162    55.7 | 14.112 % |
c |    259071 |  177392   502669 |   95229   40710  2266475    55.7 | 14.112 % |
c ==============================================================================
c [1mFound solution: 2746[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    259306 |  177438   502778 |   59146   40945  2273776    55.5 | 14.112 % |
c |    259407 |  177438   502778 |   65060   41046  2276391    55.5 | 14.107 % |
c |    259557 |  177438   502778 |   71566   41196  2286602    55.5 | 14.107 % |
c |    259782 |  177438   502778 |   78723   41421  2295246    55.4 | 14.107 % |
c |    260120 |  177438   502778 |   86595   41759  2332513    55.9 | 14.107 % |
c |    260627 |  177438   502778 |   95255   42266  2360673    55.9 | 14.107 % |
c |    261386 |  177438   502778 |  104780   43025  2411467    56.0 | 14.107 % |
c |    262525 |  177438   502778 |  115258   44164  2458048    55.7 | 14.107 % |
c ==============================================================================
c [1mFound solution: 2745[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    262695 |  177443   502789 |   59147   44334  2463525    55.6 | 14.107 % |
c |    262796 |  177443   502789 |   65061   44435  2464640    55.5 | 14.108 % |
c |    262946 |  177443   502789 |   71567   44585  2468120    55.4 | 14.108 % |
c |    263172 |  177443   502789 |   78724   44811  2475855    55.3 | 14.108 % |
c |    263509 |  177443   502789 |   86597   45148  2507269    55.5 | 14.108 % |
c |    264017 |  177443   502789 |   95256   45656  2542287    55.7 | 14.108 % |
c |    264776 |  177443   502789 |  104782   46415  2578334    55.5 | 14.108 % |
c |    265915 |  177443   502789 |  115260   47554  2704822    56.9 | 14.108 % |
c |    267626 |  177443   502789 |  126786   49265  2758039    56.0 | 14.108 % |
c |    270188 |  177443   502789 |  139465   51827  2954062    57.0 | 14.108 % |
c |    274033 |  177443   502789 |  153412   55672  3158798    56.7 | 14.108 % |
c |    279800 |  177443   502789 |  168753   61439  3443505    56.0 | 14.108 % |
c |    288449 |  177443   502789 |  185628   70088  4138981    59.1 | 14.108 % |
c |    301423 |  177443   502789 |  204191   83062  6008088    72.3 | 14.108 % |
c |    320884 |  177435   502770 |  224610  102522  7756032    75.7 | 14.113 % |
c |    350077 |  177435   502770 |  247071  131715 10552176    80.1 | 14.113 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 12414 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.91 0.95 0.90 2/54 12410
Raw data (stat): 12410 (runsolver) R 12409 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853795456 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0049 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12414
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.025 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 12455
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.026 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.027 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.027 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.028 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.029 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.029 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 12467
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.031 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.032 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.031 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.031 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.032 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.032 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.033 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.034 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.034 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.035 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.042 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12469
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.044 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.047 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.05 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.051 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.052 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.053 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.054 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.055 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.056 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.057 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.058 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.07 s]
Raw data (loadavg): 1.00 1.00 0.92 3/55 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.73 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 12471
Raw data (stat): 12410 (minisat+_script) S 12409 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853795456 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.73
CPU time (s): 1229.87
CPU user time (s): 1229.12
CPU system time (s): 0.746886
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####