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 30547

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 17:36:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21940 boxname=wulflinc28 idbench=358 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc28/normalized-ws97-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-ws97-5.opb
IDLAUNCH: 21940
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        509464 kB
Buffers:         32804 kB
Cached:         471044 kB
SwapCached:       1052 kB
Active:          59136 kB
Inactive:       447268 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        509212 kB
SwapTotal:     2097640 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5468 kB
Slab:            13188 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 17:56:34 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21940 7 1229.85 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]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
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 |   15366    52416 |    5122       0        0     nan |  0.000 % |
c |       100 |   15366    52416 |    5634     100     1484    14.8 |  8.161 % |
c |       250 |   15360    52399 |    6197     249     2148     8.6 |  8.187 % |
c |       475 |   15360    52399 |    6817     474     3249     6.9 |  8.187 % |
c |       812 |   15360    52399 |    7499     811     4637     5.7 |  8.187 % |
c |      1318 |   15354    52382 |    8249    1316     6837     5.2 |  8.212 % |
c |      2077 |   15354    52382 |    9073    2075    13992     6.7 |  8.212 % |
c |      3216 |   15354    52382 |    9981    3214    24484     7.6 |  8.212 % |
c |      4924 |   15354    52382 |   10979    4922    46561     9.5 |  8.212 % |
c ==============================================================================
c [1mFound solution: 9314[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 |      6384 |   79883   203237 |   26627    6382    77937    12.2 |  8.212 % |
c |      6484 |   79883   203237 |   29289    6482    78687    12.1 |  1.057 % |
c |      6634 |   79774   202991 |   32218    6631    79642    12.0 |  1.147 % |
c |      6859 |   74962   191937 |   35440    6753    80126    11.9 |  6.065 % |
c |      7196 |   66846   173214 |   38984    6963    80887    11.6 | 14.536 % |
c |      7703 |   66771   173045 |   42883    7469    93911    12.6 | 14.602 % |
c |      8463 |   62957   164225 |   47171    8109   100743    12.4 | 18.697 % |
c |      9602 |   60585   158744 |   51888    9196   108448    11.8 | 21.206 % |
c |     11310 |   58525   153954 |   57077   10778   126264    11.7 | 23.479 % |
c |     13872 |   57609   151828 |   62785   13275   244456    18.4 | 24.479 % |
c ==============================================================================
c [1mFound solution: 6496[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 |     16671 |   57583   151800 |   19194   16055   319180    19.9 | 24.479 % |
c |     16771 |   57583   151800 |   21113   16155   319971    19.8 | 24.737 % |
c |     16922 |   57583   151800 |   23224   16306   324485    19.9 | 24.737 % |
c |     17147 |   57569   151772 |   25547   16530   326441    19.7 | 24.760 % |
c |     17484 |   57508   151628 |   28101   16852   328167    19.5 | 24.833 % |
c |     17991 |   57508   151628 |   30912   17359   331875    19.1 | 24.833 % |
c |     18750 |   57346   151253 |   34003   18111   345001    19.0 | 25.005 % |
c |     19889 |   57195   150909 |   37403   19248   363574    18.9 | 25.144 % |
c |     21597 |   57191   150900 |   41144   20954   382129    18.2 | 25.147 % |
c ==============================================================================
c [1mFound solution: 5281[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 |     22888 |   57379   151365 |   19126   22245   421408    18.9 | 25.147 % |
c |     22990 |   57315   151216 |   21038   22338   421848    18.9 | 25.233 % |
c |     23140 |   57315   151216 |   23142   22488   423943    18.9 | 25.233 % |
c |     23365 |   57315   151216 |   25456   22713   426109    18.8 | 25.233 % |
c |     23702 |   57309   151200 |   28002   22627   424917    18.8 | 25.243 % |
c |     24211 |   57309   151200 |   30802   23136   434293    18.8 | 25.243 % |
c ==============================================================================
c [1mFound solution: 4066[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24644 |   57392   151404 |   19130   23569   440664    18.7 | 25.243 % |
c |     24744 |   57392   151404 |   21043   23669   442001    18.7 | 25.209 % |
c |     24894 |   57392   151404 |   23147   23819   443191    18.6 | 25.209 % |
c |     25119 |   57392   151404 |   25462   24044   445188    18.5 | 25.209 % |
c |     25456 |   57392   151404 |   28008   24381   448040    18.4 | 25.209 % |
c |     25963 |   57392   151404 |   30809   24888   452670    18.2 | 25.209 % |
c |     26722 |   57392   151404 |   33889   25647   461903    18.0 | 25.209 % |
c |     27862 |   57382   151380 |   37278   26786   497727    18.6 | 25.222 % |
c |     29570 |   57382   151380 |   41006   28494   558553    19.6 | 25.222 % |
c |     32133 |   57382   151380 |   45107   31057   640845    20.6 | 25.222 % |
c |     35978 |   57382   151380 |   49618   34902   779861    22.3 | 25.222 % |
c |     41744 |   57382   151380 |   54580   40668   931170    22.9 | 25.222 % |
c |     50394 |   57382   151380 |   60038   49318  1673623    33.9 | 25.222 % |
c |     63369 |   57382   151380 |   66041   62293  2223642    35.7 | 25.222 % |
c ==============================================================================
c [1mFound solution: 4060[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 |     66063 |   57591   151908 |   19197   64987  2320754    35.7 | 25.222 % |
c |     66163 |   57591   151908 |   21116   16621   568798    34.2 | 25.354 % |
c |     66313 |   57591   151908 |   23228   16771   569641    34.0 | 25.354 % |
c |     66538 |   57591   151908 |   25551   16996   571278    33.6 | 25.354 % |
c |     66875 |   57591   151908 |   28106   17333   577725    33.3 | 25.354 % |
c |     67381 |   57591   151908 |   30916   17839   585593    32.8 | 25.354 % |
c |     68140 |   57591   151908 |   34008   18598   594970    32.0 | 25.354 % |
c |     69279 |   57591   151908 |   37409   19737   624497    31.6 | 25.354 % |
c |     70987 |   57591   151908 |   41150   21445   664586    31.0 | 25.354 % |
c |     73551 |   57585   151894 |   45265   24007   739924    30.8 | 25.361 % |
c |     77397 |   57585   151894 |   49792   27853   904135    32.5 | 25.361 % |
c |     83163 |   57581   151885 |   54771   33617  1060944    31.6 | 25.364 % |
c |     91812 |   57581   151885 |   60248   42266  1452861    34.4 | 25.364 % |
c |    104786 |   57581   151885 |   66273   55240  1873147    33.9 | 25.364 % |
c |    124250 |   57581   151885 |   72900   74704  3161493    42.3 | 25.364 % |
c ==============================================================================
c [1mFound solution: 3662[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 |    133860 |   57892   152632 |   19297   21901   880710    40.2 | 25.364 % |
c |    133960 |   57892   152632 |   21226   22001   881271    40.1 | 25.539 % |
c |    134110 |   57892   152632 |   23349   22151   882042    39.8 | 25.539 % |
c |    134335 |   57892   152632 |   25684   22376   884694    39.5 | 25.539 % |
c |    134673 |   57892   152632 |   28252   22714   889418    39.2 | 25.539 % |
c |    135179 |   57892   152632 |   31078   23220   894281    38.5 | 25.539 % |
c |    135938 |   57892   152632 |   34185   23979   937228    39.1 | 25.539 % |
c |    137077 |   57892   152632 |   37604   25118   975100    38.8 | 25.539 % |
c |    138786 |   57892   152632 |   41364   26827  1027613    38.3 | 25.539 % |
c |    141349 |   57892   152632 |   45501   29390  1098481    37.4 | 25.539 % |
c |    145193 |   57892   152632 |   50051   33234  1274649    38.4 | 25.539 % |
c |    150959 |   57866   152572 |   55056   38996  1470513    37.7 | 25.574 % |
c |    159608 |   57862   152563 |   60562   47643  1747714    36.7 | 25.577 % |
c |    172582 |   57856   152549 |   66618   60615  2281298    37.6 | 25.584 % |
c ==============================================================================
c [1mFound solution: 3079[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 |    175916 |   57912   152735 |   19304   63949  2346819    36.7 | 25.584 % |
c |    176016 |   57912   152735 |   21234   19705   490210    24.9 | 25.558 % |
c |    176166 |   57906   152721 |   23357   19853   491591    24.8 | 25.565 % |
c |    176392 |   57906   152721 |   25693   20079   494326    24.6 | 25.565 % |
c |    176729 |   57906   152721 |   28262   20416   498418    24.4 | 25.565 % |
c |    177236 |   57906   152721 |   31089   20923   508410    24.3 | 25.565 % |
c |    177995 |   57906   152721 |   34198   21682   539343    24.9 | 25.565 % |
c |    179135 |   57906   152721 |   37618   22822   584468    25.6 | 25.565 % |
c |    180843 |   57906   152721 |   41379   24530   638280    26.0 | 25.565 % |
c |    183406 |   57906   152721 |   45517   27093   692449    25.6 | 25.565 % |
c |    187253 |   57906   152721 |   50069   30940   814744    26.3 | 25.565 % |
c |    193019 |   57906   152721 |   55076   36706  1077438    29.4 | 25.565 % |
c ==============================================================================
c [1mFound solution: 2868[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 |    200371 |   58129   153267 |   19376   44058  1296292    29.4 | 25.565 % |
c |    200472 |   58129   153267 |   21313   18468   445112    24.1 | 25.686 % |
c |    200626 |   58129   153267 |   23444   18622   448472    24.1 | 25.686 % |
c |    200855 |   58129   153267 |   25789   18851   454458    24.1 | 25.686 % |
c |    201194 |   58129   153267 |   28368   19190   461572    24.1 | 25.686 % |
c |    201700 |   58129   153267 |   31205   19696   477387    24.2 | 25.686 % |
c |    202459 |   58129   153267 |   34325   20455   493145    24.1 | 25.686 % |
c |    203599 |   58129   153267 |   37758   21595   528313    24.5 | 25.686 % |
c |    205307 |   58129   153267 |   41534   23303   573470    24.6 | 25.686 % |
c |    207870 |   58129   153267 |   45687   25866   672378    26.0 | 25.686 % |
c |    211714 |   58129   153267 |   50256   29710   831617    28.0 | 25.686 % |
c |    217481 |   58129   153267 |   55281   35477  1092125    30.8 | 25.686 % |
c |    226131 |   58129   153267 |   60810   44127  1425615    32.3 | 25.686 % |
c |    239107 |   58119   153241 |   66891   57100  1781631    31.2 | 25.692 % |
c |    258570 |   58119   153241 |   73580   76563  2735065    35.7 | 25.692 % |
c |    287762 |   58119   153241 |   80938   42153  1541978    36.6 | 25.692 % |
c |    331552 |   58119   153241 |   89032   85943  3287901    38.3 | 25.692 % |
c |    397236 |   58119   153241 |   97935   70548  3636854    51.6 | 25.692 % |
c ==============================================================================
c [1mFound solution: 2861[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 |    415642 |   58128   153266 |   19376   88954  4336669    48.8 | 25.692 % |
c |    415742 |   58128   153266 |   21313   18890   451232    23.9 | 25.692 % |
c |    415893 |   58128   153266 |   23444   19041   452115    23.7 | 25.692 % |
c |    416118 |   58128   153266 |   25789   19266   455736    23.7 | 25.692 % |
c |    416457 |   58128   153266 |   28368   19605   460675    23.5 | 25.692 % |
c |    416963 |   58128   153266 |   31205   20111   466605    23.2 | 25.692 % |
c |    417724 |   58128   153266 |   34325   20872   480064    23.0 | 25.692 % |
c |    418863 |   58128   153266 |   37758   22011   515414    23.4 | 25.692 % |
c |    420571 |   58128   153266 |   41534   23719   554657    23.4 | 25.692 % |
c |    423133 |   58128   153266 |   45687   26281   642001    24.4 | 25.692 % |
c |    426977 |   58128   153266 |   50256   30125   761954    25.3 | 25.692 % |
c ==============================================================================
c [1mFound solution: 2851[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 |    429829 |   58134   153280 |   19378   32977   842818    25.6 | 25.692 % |
c |    429931 |   58134   153280 |   21315   16591   334500    20.2 | 25.692 % |
c |    430081 |   58134   153280 |   23447   16741   336379    20.1 | 25.692 % |
c |    430306 |   58134   153280 |   25792   16966   339018    20.0 | 25.692 % |
c |    430643 |   58134   153280 |   28371   17303   344233    19.9 | 25.692 % |
c |    431149 |   58134   153280 |   31208   17809   352370    19.8 | 25.692 % |
c |    431908 |   58134   153280 |   34329   18568   366241    19.7 | 25.692 % |
c |    433050 |   58134   153280 |   37762   19710   407841    20.7 | 25.692 % |
c |    434759 |   58134   153280 |   41538   21419   467633    21.8 | 25.692 % |
c |    437321 |   58134   153280 |   45692   23981   538765    22.5 | 25.692 % |
c |    441165 |   58134   153280 |   50261   27825   683990    24.6 | 25.692 % |
c |    446932 |   58134   153280 |   55287   33592   881186    26.2 | 25.692 % |
c |    455584 |   58134   153280 |   60816   42244  1186549    28.1 | 25.692 % |
c |    468558 |   58134   153280 |   66898   55218  1666272    30.2 | 25.692 % |
c |    488020 |   58134   153280 |   73587   74680  2696073    36.1 | 25.692 % |
c |    517212 |   58134   153280 |   80946   41235  1451208    35.2 | 25.692 % |
c |    561002 |   58134   153280 |   89041   85025  3444853    40.5 | 25.692 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  7321 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.95 2/54 7317
Raw data (stat): 7317 (runsolver) R 7316 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 840732857 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.93 0.95 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0007 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0009 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0017 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.001 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0021 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.72 s]
Raw data (loadavg): 0.99 0.97 0.95 1/53 7321
Raw data (stat): 7317 (minisat+_script) S 7316 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 840732857 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.72
CPU time (s): 1229.85
CPU user time (s): 1229.32
CPU system time (s): 0.532918
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####