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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-4.opb
MD5SUM417d3abd60fd3b9eb4200ff5119a92c4
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 818
Optimality of the best value was proved NO
Number of terms in the objective function 1798
Biggest coefficient in the objective function 349
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 104116
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 349
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 104116
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1267.1
Number of variables2289
Total number of constraints3052
Number of constraints which are clauses360
Number of constraints which are cardinality constraints (but not clauses)2692
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint195

Trace number 2340

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-18 19:05:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2726 boxname=wulflinc21 idbench=382 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  417d3abd60fd3b9eb4200ff5119a92c4  /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb
IDLAUNCH: 2726
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        894868 kB
Buffers:         35108 kB
Cached:          77476 kB
SwapCached:        908 kB
Active:          79100 kB
Inactive:        36196 kB
HighTotal:      131008 kB
HighFree:        57288 kB
LowTotal:       903652 kB
LowFree:        837580 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            18840 kB
Committed_AS:    64332 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:25:42 (client local time) WITH STATUS 0 IN 1207.69 SECONDS
stats: 2726 7 1207.69 0

Solver Data

c Parsing PB file...
c Converting 1139 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................
c ---[1138]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1137]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1136]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1135]---> Adder-cost: 352   maxlim: 131   bits: 8/8
c ---[1134]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1133]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1132]---> Adder-cost: 382   maxlim: 168   bits: 8/8
c ---[1131]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1130]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1129]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1128]---> Adder-cost: 382   maxlim: 168   bits: 8/8
c ---[1127]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1126]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1125]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1124]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1123]---> Adder-cost: 32   maxlim: 35   bits: 7/6
c ---[1122]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1121]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1120]---> Adder-cost: 20   maxlim: 18   bits: 6/5
c ---[1119]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1118]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1117]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1116]---> Adder-cost: 20   maxlim: 18   bits: 6/5
c ---[1115]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   13
c ---[1109]---> BDD-cost:    5
c ---[1107]---> BDD-cost:   13
c ---[1105]---> BDD-cost:    5
c ---[1103]---> BDD-cost:   13
c ---[1101]---> BDD-cost:    5
c ---[1099]---> BDD-cost:   13
c ---[1097]---> BDD-cost:    5
c ---[1095]---> BDD-cost:   13
c ---[1093]---> BDD-cost:    5
c ---[1091]---> BDD-cost:   13
c ---[1089]---> BDD-cost:    5
c ---[1087]---> BDD-cost:   13
c ---[1085]---> BDD-cost:    5
c ---[1083]---> BDD-cost:   13
c ---[1081]---> BDD-cost:    5
c ---[1079]---> BDD-cost:   13
c ---[1077]---> BDD-cost:    5
c ---[1075]---> BDD-cost:   13
c ---[1073]---> BDD-cost:    5
c ---[1071]---> BDD-cost:   13
c ---[1069]---> BDD-cost:    5
c ---[1067]---> BDD-cost:   13
c ---[1065]---> BDD-cost:    5
c ---[1063]---> BDD-cost:   13
c ---[1061]---> BDD-cost:    5
c ---[1059]---> BDD-cost:   13
c ---[1057]---> BDD-cost:    5
c ---[1055]---> BDD-cost:   13
c ---[1053]---> BDD-cost:    5
c ---[1051]---> BDD-cost:   13
c ---[1049]---> BDD-cost:    5
c ---[1047]---> BDD-cost:   13
c ---[1045]---> BDD-cost:    5
c ---[1043]---> BDD-cost:   13
c ---[1041]---> BDD-cost:    5
c ---[1039]---> BDD-cost:   13
c ---[1037]---> BDD-cost:    5
c ---[1035]---> BDD-cost:   13
c ---[1033]---> BDD-cost:    5
c ---[1031]---> BDD-cost:   13
c ---[1029]---> BDD-cost:    5
c ---[1027]---> BDD-cost:   13
c ---[1025]---> BDD-cost:    5
c ---[1023]---> BDD-cost:   13
c ---[1021]---> BDD-cost:    5
c ---[1019]---> BDD-cost:   13
c ---[1017]---> BDD-cost:    5
c ---[1015]---> BDD-cost:   13
c ---[1013]---> BDD-cost:    5
c ---[1011]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1007]---> BDD-cost:    5
c ---[1005]---> BDD-cost:   13
c ---[1003]---> BDD-cost:    5
c ---[1001]---> BDD-cost:   13
c ---[ 999]---> BDD-cost:    5
c ---[ 997]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:    5
c ---[ 993]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:    5
c ---[ 987]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:    5
c ---[ 983]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:    5
c ---[ 979]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:    5
c ---[ 975]---> BDD-cost:   13
c ---[ 973]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:   13
c ---[ 969]---> BDD-cost:    5
c ---[ 967]---> BDD-cost:   13
c ---[ 965]---> BDD-cost:    5
c ---[ 963]---> BDD-cost:   13
c ---[ 961]---> BDD-cost:    5
c ---[ 959]---> BDD-cost:   13
c ---[ 957]---> BDD-cost:    5
c ---[ 955]---> BDD-cost:   13
c ---[ 953]---> BDD-cost:    5
c ---[ 951]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:    5
c ---[ 947]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:    5
c ---[ 943]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:    5
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:    5
c ---[ 935]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:    5
c ---[ 931]---> BDD-cost:   13
c ---[ 929]---> BDD-cost:    5
c ---[ 927]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:    5
c ---[ 923]---> BDD-cost:   13
c ---[ 921]---> BDD-cost:    5
c ---[ 919]---> BDD-cost:   13
c ---[ 917]---> BDD-cost:    5
c ---[ 915]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:    5
c ---[ 911]---> BDD-cost:   13
c ---[ 909]---> BDD-cost:    5
c ---[ 907]---> BDD-cost:   13
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:    5
c ---[ 901]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:    5
c ---[ 897]---> BDD-cost:   13
c ---[ 895]---> BDD-cost:    5
c ---[ 893]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:    5
c ---[ 889]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:    5
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:    5
c ---[ 881]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:    5
c ---[ 877]---> BDD-cost:   13
c ---[ 875]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:   13
c ---[ 871]---> BDD-cost:    5
c ---[ 869]---> BDD-cost:   13
c ---[ 867]---> BDD-cost:    5
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:    5
c ---[ 861]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:    5
c ---[ 857]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:    5
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:    5
c ---[ 849]---> BDD-cost:   13
c ---[ 847]---> BDD-cost:    5
c ---[ 845]---> BDD-cost:   13
c ---[ 843]---> BDD-cost:    5
c ---[ 841]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:    5
c ---[ 837]---> BDD-cost:   13
c ---[ 835]---> BDD-cost:    5
c ---[ 833]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:    5
c ---[ 825]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:    5
c ---[ 815]---> BDD-cost:   13
c ---[ 813]---> BDD-cost:    5
c ---[ 811]---> BDD-cost:   13
c ---[ 809]---> BDD-cost:    5
c ---[ 807]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:    5
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:    5
c ---[ 799]---> BDD-cost:   13
c ---[ 797]---> BDD-cost:    5
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   13
c ---[ 791]---> BDD-cost:    5
c ---[ 789]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:   13
c ---[ 783]---> BDD-cost:   13
c ---[ 781]---> BDD-cost:    5
c ---[ 779]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:    5
c ---[ 775]---> BDD-cost:   13
c ---[ 773]---> BDD-cost:    5
c ---[ 771]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:    5
c ---[ 767]---> BDD-cost:   13
c ---[ 765]---> BDD-cost:    5
c ---[ 763]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:    5
c ---[ 757]---> BDD-cost:   13
c ---[ 755]---> BDD-cost:    5
c ---[ 753]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:    5
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:    5
c ---[ 745]---> BDD-cost:   13
c ---[ 743]---> BDD-cost:    5
c ---[ 741]---> BDD-cost:   13
c ---[ 739]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:   13
c ---[ 735]---> BDD-cost:    5
c ---[ 733]---> BDD-cost:   13
c ---[ 731]---> BDD-cost:    5
c ---[ 729]---> BDD-cost:   13
c ---[ 727]---> BDD-cost:    5
c ---[ 725]---> BDD-cost:   13
c ---[ 723]---> BDD-cost:    5
c ---[ 721]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:   13
c ---[ 715]---> BDD-cost:   13
c ---[ 713]---> BDD-cost:    5
c ---[ 711]---> BDD-cost:   13
c ---[ 709]---> BDD-cost:   13
c ---[ 707]---> BDD-cost:    5
c ---[ 705]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:    5
c ---[ 693]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:    5
c ---[ 689]---> BDD-cost:   13
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:    5
c ---[ 681]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:    5
c ---[ 677]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:    5
c ---[ 673]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:    5
c ---[ 669]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:   13
c ---[ 663]---> BDD-cost:    5
c ---[ 661]---> BDD-cost:   13
c ---[ 659]---> BDD-cost:    5
c ---[ 657]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:    5
c ---[ 653]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:    5
c ---[ 649]---> BDD-cost:   13
c ---[ 647]---> BDD-cost:    5
c ---[ 645]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:    5
c ---[ 641]---> BDD-cost:   13
c ---[ 639]---> BDD-cost:    5
c ---[ 637]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:    5
c ---[ 629]---> BDD-cost:   13
c ---[ 627]---> BDD-cost:    5
c ---[ 625]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:   13
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:   13
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:   13
c ---[ 607]---> BDD-cost:    5
c ---[ 605]---> BDD-cost:   13
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    1
c ---[ 599]---> BDD-cost:    5
c ---[ 597]---> BDD-cost:   13
c ---[ 595]---> BDD-cost:    5
c ---[ 593]---> BDD-cost:   13
c ---[ 591]---> BDD-cost:    5
c ---[ 589]---> BDD-cost:   13
c ---[ 587]---> BDD-cost:    5
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:   13
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:   13
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:   13
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:   13
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:   13
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:   13
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:   13
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:   13
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:   13
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:   13
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:   13
c ---[ 537]---> BDD-cost:   13
c ---[ 535]---> BDD-cost:    5
c ---[ 533]---> BDD-cost:   13
c ---[ 531]---> BDD-cost:    5
c ---[ 529]---> BDD-cost:   13
c ---[ 527]---> BDD-cost:    5
c ---[ 525]---> BDD-cost:   13
c ---[ 523]---> BDD-cost:    5
c ---[ 521]---> BDD-cost:   13
c ---[ 519]---> BDD-cost:    5
c ---[ 517]---> BDD-cost:   13
c ---[ 515]---> BDD-cost:   13
c ---[ 513]---> BDD-cost:   13
c ---[ 511]---> BDD-cost:   13
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:   13
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:   13
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:   13
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:   13
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:   13
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:   13
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:   13
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:   13
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:   13
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:   13
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:   13
c ---[ 465]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:   13
c ---[ 461]---> BDD-cost:    5
c ---[ 459]---> BDD-cost:   13
c ---[ 457]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:   13
c ---[ 453]---> BDD-cost:    5
c ---[ 451]---> BDD-cost:   13
c ---[ 449]---> BDD-cost:    5
c ---[ 447]---> BDD-cost:   13
c ---[ 445]---> BDD-cost:    5
c ---[ 443]---> BDD-cost:   13
c ---[ 441]---> BDD-cost:    5
c ---[ 439]---> BDD-cost:   13
c ---[ 437]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:   13
c ---[ 433]---> BDD-cost:    5
c ---[ 431]---> BDD-cost:   13
c ---[ 429]---> BDD-cost:    5
c ---[ 427]---> BDD-cost:   13
c ---[ 425]---> BDD-cost:    5
c ---[ 423]---> BDD-cost:   13
c ---[ 421]---> BDD-cost:    5
c ---[ 419]---> BDD-cost:   13
c ---[ 417]---> BDD-cost:    5
c ---[ 415]---> BDD-cost:   13
c ---[ 413]---> BDD-cost:   13
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:   13
c ---[ 407]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:   13
c ---[ 403]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   13
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:   13
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:   13
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:   13
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:   13
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:   13
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:   13
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:   13
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:   13
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:   13
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:   13
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42588   143418 |   14196       0        0     nan |  0.000 % |
c |       100 |   42588   143418 |   15615     100     1381    13.8 |  4.341 % |
c |       250 |   42583   143405 |   17177     248     1825     7.4 |  4.360 % |
c |       476 |   42562   143336 |   18894     468     2925     6.2 |  4.387 % |
c |       813 |   42546   143282 |   20784     803     5007     6.2 |  4.406 % |
c |      1319 |   42513   143171 |   22862    1301     7660     5.9 |  4.462 % |
c |      2079 |   42487   143083 |   25149    2048    11155     5.4 |  4.508 % |
c |      3220 |   42465   143013 |   27663    3175    21980     6.9 |  4.545 % |
c |      4928 |   42404   142811 |   30430    4729    29647     6.3 |  4.676 % |
c |      7490 |   42302   142471 |   33473    7244    85196    11.8 |  4.852 % |
c |     11334 |   42240   142263 |   36820   11072   126027    11.4 |  4.954 % |
c |     17100 |   42234   142243 |   40502   14819   191852    12.9 |  4.982 % |
c |     25750 |   42234   142243 |   44553   23469   868690    37.0 |  4.982 % |
c |     38724 |   42234   142243 |   49008   36443  2774011    76.1 |  4.982 % |
c |     58186 |   42234   142243 |   53909   16247   841211    51.8 |  4.982 % |
c |     87380 |   42225   142212 |   59300   45438  3613633    79.5 |  4.992 % |
c |    131169 |   42181   142066 |   65230   40602  1529090    37.7 |  5.112 % |
c |    196854 |   42181   142066 |   71753   50993  6418011   125.9 |  5.112 % |
c |    295380 |   42181   142066 |   78928   29223  7186333   245.9 |  5.112 % |
c |    443169 |   42181   142066 |   86821   45867 13533259   295.1 |  5.112 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/30972/stat): 30972 (minisat+_script) R 30971 30972 20602 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1720908837 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/30972/statm): 174 3 169 147 0 27 0
[pid=30972] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=30973
New process pid=30974
New process pid=30975
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=30974) exited with status: 0
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=30975) exited with status: 0
One traced child (pid=30973) exited with status: 0
New process pid=30976
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.95 0.90 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 1415 0 0 0 983 7 0 0 25 0 1 0 1720908842 6316032 1360 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 1542 1360 145 145 0 1397 0
[pid=30976] vsize: 6168
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 8292

[startup+20.0038 s]
Raw data (loadavg): 0.94 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 2536 0 0 0 1968 13 0 0 25 0 1 0 1720908842 10903552 2481 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 2662 2481 145 145 0 2517 0
[pid=30976] vsize: 10648
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 12772

[startup+30.0044 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 3902 0 0 0 2947 23 0 0 25 0 1 0 1720908842 16609280 3847 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 4055 3847 145 145 0 3910 0
[pid=30976] vsize: 16220
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 18344

[startup+40.0051 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5049 0 0 0 3932 29 0 0 25 0 1 0 1720908842 21237760 4994 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 5185 4994 145 145 0 5040 0
[pid=30976] vsize: 20740
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 22864

[startup+50.0058 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 4926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0
[pid=30976] vsize: 22180
Current children cumulated CPU time (s) 49.6
Current children cumulated vsize (Kb) 24304

[startup+60.0065 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 5926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0
[pid=30976] vsize: 22180
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 24304

[startup+70.0071 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 5406 0 0 0 6926 33 0 0 25 0 1 0 1720908842 22712320 5351 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 5545 5351 145 145 0 5400 0
[pid=30976] vsize: 22180
Current children cumulated CPU time (s) 69.6
Current children cumulated vsize (Kb) 24304

[startup+80.0078 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6032 0 0 0 7917 37 0 0 25 0 1 0 1720908842 25268224 5977 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 6169 5977 145 145 0 6024 0
[pid=30976] vsize: 24676
Current children cumulated CPU time (s) 79.55
Current children cumulated vsize (Kb) 26800

[startup+90.0085 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 8912 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0
[pid=30976] vsize: 25928
Current children cumulated CPU time (s) 89.52
Current children cumulated vsize (Kb) 28052

[startup+100.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 9913 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0
[pid=30976] vsize: 25928
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 28052

[startup+110.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6347 0 0 0 10913 39 0 0 25 0 1 0 1720908842 26550272 6292 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 6482 6292 145 145 0 6337 0
[pid=30976] vsize: 25928
Current children cumulated CPU time (s) 109.53
Current children cumulated vsize (Kb) 28052

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6348 0 0 0 11913 39 0 0 25 0 1 0 1720908842 26550272 6293 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 6482 6293 145 145 0 6337 0
[pid=30976] vsize: 25928
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 28052

[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 12906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0
[pid=30976] vsize: 28044
Current children cumulated CPU time (s) 129.48
Current children cumulated vsize (Kb) 30168

[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 13906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0
[pid=30976] vsize: 28044
Current children cumulated CPU time (s) 139.48
Current children cumulated vsize (Kb) 30168

[startup+150.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 6819 0 0 0 14906 41 0 0 25 0 1 0 1720908842 28717056 6764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 7011 6764 145 145 0 6866 0
[pid=30976] vsize: 28044
Current children cumulated CPU time (s) 149.48
Current children cumulated vsize (Kb) 30168

[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 7937 0 0 0 15887 49 0 0 25 0 1 0 1720908842 33296384 7882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 8129 7882 145 145 0 7984 0
[pid=30976] vsize: 32516
Current children cumulated CPU time (s) 159.37
Current children cumulated vsize (Kb) 34640

[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 8918 0 0 0 16870 55 0 0 25 0 1 0 1720908842 37318656 8863 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 9111 8863 145 145 0 8966 0
[pid=30976] vsize: 36444
Current children cumulated CPU time (s) 169.26
Current children cumulated vsize (Kb) 38568

[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 9847 0 0 0 17854 62 0 0 25 0 1 0 1720908842 41123840 9792 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 10040 9792 145 145 0 9895 0
[pid=30976] vsize: 40160
Current children cumulated CPU time (s) 179.17
Current children cumulated vsize (Kb) 42284

[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 10706 0 0 0 18841 67 0 0 25 0 1 0 1720908842 44642304 10651 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 10899 10651 145 145 0 10754 0
[pid=30976] vsize: 43596
Current children cumulated CPU time (s) 189.09
Current children cumulated vsize (Kb) 45720

[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 19834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 199.05
Current children cumulated vsize (Kb) 47580

[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 20834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 209.05
Current children cumulated vsize (Kb) 47580

[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 21834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 219.05
Current children cumulated vsize (Kb) 47580

[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 22834 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 229.05
Current children cumulated vsize (Kb) 47580

[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 23835 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 239.06
Current children cumulated vsize (Kb) 47580

[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11176 0 0 0 24835 70 0 0 25 0 1 0 1720908842 46546944 11121 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11121 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 249.06
Current children cumulated vsize (Kb) 47580

[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 25835 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 259.06
Current children cumulated vsize (Kb) 47580

[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 26835 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 269.06
Current children cumulated vsize (Kb) 47580

[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 27836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 279.07
Current children cumulated vsize (Kb) 47580

[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 28836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 289.07
Current children cumulated vsize (Kb) 47580

[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 29836 70 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223060 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 299.07
Current children cumulated vsize (Kb) 47580

[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11178 0 0 0 30835 71 0 0 25 0 1 0 1720908842 46546944 11123 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 11364 11123 145 145 0 11219 0
[pid=30976] vsize: 45456
Current children cumulated CPU time (s) 309.07
Current children cumulated vsize (Kb) 47580

[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 11864 0 0 0 31824 75 0 0 25 0 1 0 1720908842 49364992 11809 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 12052 11809 145 145 0 11907 0
[pid=30976] vsize: 48208
Current children cumulated CPU time (s) 319
Current children cumulated vsize (Kb) 50332

[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 12858 0 0 0 32806 83 0 0 25 0 1 0 1720908842 53428224 12803 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30976/statm): 13044 12803 145 145 0 12899 0
[pid=30976] vsize: 52176
Current children cumulated CPU time (s) 328.9
Current children cumulated vsize (Kb) 54300

[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 13828 0 0 0 33790 90 0 0 25 0 1 0 1720908842 57438208 13773 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 14023 13773 145 145 0 13878 0
[pid=30976] vsize: 56092
Current children cumulated CPU time (s) 338.81
Current children cumulated vsize (Kb) 58216

[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 14636 0 0 0 34777 95 0 0 25 0 1 0 1720908842 60776448 14581 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 14838 14581 145 145 0 14693 0
[pid=30976] vsize: 59352
Current children cumulated CPU time (s) 348.73
Current children cumulated vsize (Kb) 61476

[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 15309 0 0 0 35767 99 0 0 25 0 1 0 1720908842 63545344 15254 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 15514 15254 145 145 0 15369 0
[pid=30976] vsize: 62056
Current children cumulated CPU time (s) 358.67
Current children cumulated vsize (Kb) 64180

[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) T 30972 30972 20602 0 -1 0 16034 0 0 0 36756 104 0 0 25 0 1 0 1720908842 66502656 15979 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/30976/statm): 16236 15979 145 145 0 16091 0
[pid=30976] vsize: 64944
Current children cumulated CPU time (s) 368.61
Current children cumulated vsize (Kb) 67068

[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 37740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 378.51
Current children cumulated vsize (Kb) 70980

[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 38740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 388.51
Current children cumulated vsize (Kb) 70980

[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 39740 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 398.51
Current children cumulated vsize (Kb) 70980

[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 40741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 408.52
Current children cumulated vsize (Kb) 70980

[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 41741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 418.52
Current children cumulated vsize (Kb) 70980

[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 42741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 428.52
Current children cumulated vsize (Kb) 70980

[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 43741 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 438.52
Current children cumulated vsize (Kb) 70980

[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 44742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 448.53
Current children cumulated vsize (Kb) 70980

[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 45742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134551906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 458.53
Current children cumulated vsize (Kb) 70980

[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 46742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 468.53
Current children cumulated vsize (Kb) 70980

[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 47742 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 478.53
Current children cumulated vsize (Kb) 70980

[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17018 0 0 0 48743 110 0 0 25 0 1 0 1720908842 70508544 16963 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17214 16963 145 145 0 17069 0
[pid=30976] vsize: 68856
Current children cumulated CPU time (s) 488.54
Current children cumulated vsize (Kb) 70980

[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 17251 0 0 0 49739 112 0 0 25 0 1 0 1720908842 71462912 17196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 17447 17196 145 145 0 17302 0
[pid=30976] vsize: 69788
Current children cumulated CPU time (s) 498.52
Current children cumulated vsize (Kb) 71912

[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 18079 0 0 0 50725 118 0 0 25 0 1 0 1720908842 74862592 18024 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 18277 18024 145 145 0 18132 0
[pid=30976] vsize: 73108
Current children cumulated CPU time (s) 508.44
Current children cumulated vsize (Kb) 75232

[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 18629 0 0 0 51715 122 0 0 25 0 1 0 1720908842 77119488 18574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 18828 18574 145 145 0 18683 0
[pid=30976] vsize: 75312
Current children cumulated CPU time (s) 518.38
Current children cumulated vsize (Kb) 77436

[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 19152 0 0 0 52705 126 0 0 25 0 1 0 1720908842 79269888 19097 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 19353 19097 145 145 0 19208 0
[pid=30976] vsize: 77412
Current children cumulated CPU time (s) 528.32
Current children cumulated vsize (Kb) 79536

[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 19882 0 0 0 53693 131 0 0 25 0 1 0 1720908842 82255872 19827 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 20082 19827 145 145 0 19937 0
[pid=30976] vsize: 80328
Current children cumulated CPU time (s) 538.25
Current children cumulated vsize (Kb) 82452

[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 20538 0 0 0 54684 134 0 0 25 0 1 0 1720908842 84955136 20483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 20741 20483 145 145 0 20596 0
[pid=30976] vsize: 82964
Current children cumulated CPU time (s) 548.19
Current children cumulated vsize (Kb) 85088

[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 21167 0 0 0 55673 138 0 0 25 0 1 0 1720908842 87539712 21112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 21372 21112 145 145 0 21227 0
[pid=30976] vsize: 85488
Current children cumulated CPU time (s) 558.12
Current children cumulated vsize (Kb) 87612

[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 21794 0 0 0 56661 143 0 0 25 0 1 0 1720908842 90120192 21739 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 22002 21739 145 145 0 21857 0
[pid=30976] vsize: 88008
Current children cumulated CPU time (s) 568.05
Current children cumulated vsize (Kb) 90132

[startup+580.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 22375 0 0 0 57654 146 0 0 25 0 1 0 1720908842 92495872 22320 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 22582 22320 145 145 0 22437 0
[pid=30976] vsize: 90328
Current children cumulated CPU time (s) 578.01
Current children cumulated vsize (Kb) 92452

[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 22943 0 0 0 58645 149 0 0 25 0 1 0 1720908842 94822400 22888 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 23150 22888 145 145 0 23005 0
[pid=30976] vsize: 92600
Current children cumulated CPU time (s) 587.95
Current children cumulated vsize (Kb) 94724

[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 23511 0 0 0 59634 154 0 0 25 0 1 0 1720908842 97157120 23456 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 23720 23456 145 145 0 23575 0
[pid=30976] vsize: 94880
Current children cumulated CPU time (s) 597.89
Current children cumulated vsize (Kb) 97004

[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 24005 0 0 0 60627 157 0 0 25 0 1 0 1720908842 99192832 23950 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 24217 23950 145 145 0 24072 0
[pid=30976] vsize: 96868
Current children cumulated CPU time (s) 607.85
Current children cumulated vsize (Kb) 98992

[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 24554 0 0 0 61617 161 0 0 25 0 1 0 1720908842 101441536 24499 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 24766 24499 145 145 0 24621 0
[pid=30976] vsize: 99064
Current children cumulated CPU time (s) 617.79
Current children cumulated vsize (Kb) 101188

[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 25138 0 0 0 62608 164 0 0 25 0 1 0 1720908842 103833600 25083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 25350 25083 145 145 0 25205 0
[pid=30976] vsize: 101400
Current children cumulated CPU time (s) 627.73
Current children cumulated vsize (Kb) 103524

[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 25772 0 0 0 63599 169 0 0 25 0 1 0 1720908842 106434560 25717 4294967295 134512640 135094434 3221224448 3221223104 134555975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 25985 25717 145 145 0 25840 0
[pid=30976] vsize: 103940
Current children cumulated CPU time (s) 637.69
Current children cumulated vsize (Kb) 106064

[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26286 0 0 0 64590 172 0 0 25 0 1 0 1720908842 108552192 26231 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26502 26231 145 145 0 26357 0
[pid=30976] vsize: 106008
Current children cumulated CPU time (s) 647.63
Current children cumulated vsize (Kb) 108132

[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 65586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 657.61
Current children cumulated vsize (Kb) 109320

[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 66586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 667.61
Current children cumulated vsize (Kb) 109320

[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 67586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 677.61
Current children cumulated vsize (Kb) 109320

[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26583 0 0 0 68586 174 0 0 25 0 1 0 1720908842 109768704 26528 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26528 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 687.61
Current children cumulated vsize (Kb) 109320

[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26584 0 0 0 69586 175 0 0 25 0 1 0 1720908842 109768704 26529 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26529 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 697.62
Current children cumulated vsize (Kb) 109320

[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 70587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 707.63
Current children cumulated vsize (Kb) 109320

[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 71587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 717.63
Current children cumulated vsize (Kb) 109320

[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 72587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 727.63
Current children cumulated vsize (Kb) 109320

[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 73587 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 737.63
Current children cumulated vsize (Kb) 109320

[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 74588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 747.64
Current children cumulated vsize (Kb) 109320

[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 75588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 757.64
Current children cumulated vsize (Kb) 109320

[startup+770.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 76588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223060 134563140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 767.64
Current children cumulated vsize (Kb) 109320

[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 77588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 777.64
Current children cumulated vsize (Kb) 109320

[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 78588 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 787.64
Current children cumulated vsize (Kb) 109320

[startup+800.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 79589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 797.65
Current children cumulated vsize (Kb) 109320

[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 80589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 807.65
Current children cumulated vsize (Kb) 109320

[startup+820.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 81589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 817.65
Current children cumulated vsize (Kb) 109320

[startup+830.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26585 0 0 0 82589 175 0 0 25 0 1 0 1720908842 109768704 26530 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26530 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 827.65
Current children cumulated vsize (Kb) 109320

[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26587 0 0 0 83589 175 0 0 25 0 1 0 1720908842 109768704 26532 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26532 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 837.65
Current children cumulated vsize (Kb) 109320

[startup+850.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26589 0 0 0 84590 175 0 0 25 0 1 0 1720908842 109768704 26534 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26534 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 847.66
Current children cumulated vsize (Kb) 109320

[startup+860.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26592 0 0 0 85590 175 0 0 25 0 1 0 1720908842 109768704 26537 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26537 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 857.66
Current children cumulated vsize (Kb) 109320

[startup+870.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 86590 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 867.66
Current children cumulated vsize (Kb) 109320

[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 87590 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 877.66
Current children cumulated vsize (Kb) 109320

[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 88591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 887.67
Current children cumulated vsize (Kb) 109320

[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 89591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 897.67
Current children cumulated vsize (Kb) 109320

[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 90591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 907.67
Current children cumulated vsize (Kb) 109320

[startup+920.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 91591 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 917.67
Current children cumulated vsize (Kb) 109320

[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 92592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 927.68
Current children cumulated vsize (Kb) 109320

[startup+940.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 93592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 937.68
Current children cumulated vsize (Kb) 109320

[startup+950.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 94592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 947.68
Current children cumulated vsize (Kb) 109320

[startup+960.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 95592 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 957.68
Current children cumulated vsize (Kb) 109320

[startup+970.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 96593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 967.69
Current children cumulated vsize (Kb) 109320

[startup+980.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 97593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 977.69
Current children cumulated vsize (Kb) 109320

[startup+990.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 98593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 987.69
Current children cumulated vsize (Kb) 109320

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 99593 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 997.69
Current children cumulated vsize (Kb) 109320

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 100594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1007.7
Current children cumulated vsize (Kb) 109320

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 101594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1017.7
Current children cumulated vsize (Kb) 109320

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 102594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1027.7
Current children cumulated vsize (Kb) 109320

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 103594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1037.7
Current children cumulated vsize (Kb) 109320

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 104594 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1047.7
Current children cumulated vsize (Kb) 109320

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 105595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1057.71
Current children cumulated vsize (Kb) 109320

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 106595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1067.71
Current children cumulated vsize (Kb) 109320

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 107595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1077.71
Current children cumulated vsize (Kb) 109320

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 108595 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1087.71
Current children cumulated vsize (Kb) 109320

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26594 0 0 0 109596 175 0 0 25 0 1 0 1720908842 109768704 26539 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26539 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1097.72
Current children cumulated vsize (Kb) 109320

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 110596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1107.72
Current children cumulated vsize (Kb) 109320

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 111596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1117.72
Current children cumulated vsize (Kb) 109320

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 112596 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1127.72
Current children cumulated vsize (Kb) 109320

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26595 0 0 0 113597 175 0 0 25 0 1 0 1720908842 109768704 26540 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 26799 26540 145 145 0 26654 0
[pid=30976] vsize: 107196
Current children cumulated CPU time (s) 1137.73
Current children cumulated vsize (Kb) 109320

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 26817 0 0 0 114593 177 0 0 25 0 1 0 1720908842 110678016 26762 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27021 26762 145 145 0 26876 0
[pid=30976] vsize: 108084
Current children cumulated CPU time (s) 1147.71
Current children cumulated vsize (Kb) 110208

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27325 0 0 0 115584 181 0 0 25 0 1 0 1720908842 112787456 27270 4294967295 134512640 135094434 3221224448 3221223060 134563124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27536 27270 145 145 0 27391 0
[pid=30976] vsize: 110144
Current children cumulated CPU time (s) 1157.66
Current children cumulated vsize (Kb) 112268

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27465 0 0 0 116582 181 0 0 25 0 1 0 1720908842 113381376 27410 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27681 27410 145 145 0 27536 0
[pid=30976] vsize: 110724
Current children cumulated CPU time (s) 1167.64
Current children cumulated vsize (Kb) 112848

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 117579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221222928 134780803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0
[pid=30976] vsize: 111652
Current children cumulated CPU time (s) 1177.63
Current children cumulated vsize (Kb) 113776

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 118579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0
[pid=30976] vsize: 111652
Current children cumulated CPU time (s) 1187.63
Current children cumulated vsize (Kb) 113776

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 119579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0
[pid=30976] vsize: 111652
Current children cumulated CPU time (s) 1197.63
Current children cumulated vsize (Kb) 113776

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 120579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0
[pid=30976] vsize: 111652
Current children cumulated CPU time (s) 1207.63
Current children cumulated vsize (Kb) 113776



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30976
Raw data (/proc/30972/stat): 30972 (minisat+_script) S 30971 30972 20602 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1720908837 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30972/statm): 531 226 485 147 0 384 0
[pid=30972] vsize: 2124
Raw data (/proc/30976/stat): 30976 (minisat+_64-bit) R 30972 30972 20602 0 -1 0 27695 0 0 0 120579 183 0 0 25 0 1 0 1720908842 114331648 27640 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30976/statm): 27913 27640 145 145 0 27768 0
[pid=30976] vsize: 111652
Current children cumulated CPU time (s) 1207.63
Current children cumulated vsize (Kb) 113776

Sending SIGTERM to -30972
Sleeping 2 seconds
One traced child (pid=30972) ended because it received signal 15 (SIGTERM)
One traced child (pid=30976) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.13
CPU time (s): 1207.69
CPU user time (s): 1205.8
CPU system time (s): 1.88471
CPU usage (%): 99.7982
Max. virtual memory (cumulated for all children) (Kb): 113776

Verifier Data

ERROR: no interpretation found !