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

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-nsrand-ipx.opb
MD5SUM3c0f03289c4bde51025003af805c294c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 2355200
Number of bits of the biggest number in a constraint 22
Biggest sum of numbers in a constraint 2939977599
Number of bits of the biggest sum of numbers32
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark101.672
Number of variables6641
Total number of constraints7355
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)6951
Number of constraints which are nor clauses,nor cardinality constraints404
Minimum length of a constraint1
Maximum length of a constraint6641

Trace number 6176

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-20 04:09:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3340 boxname=wulflinc18 idbench=996 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c0f03289c4bde51025003af805c294c  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-nsrand-ipx.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-nsrand-ipx.opb
IDLAUNCH: 3340
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        852648 kB
Buffers:         26484 kB
Cached:         122324 kB
SwapCached:        860 kB
Active:          41004 kB
Inactive:       110412 kB
HighTotal:      131008 kB
HighFree:        23156 kB
LowTotal:       903652 kB
LowFree:        829492 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            24948 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:29:13 (client local time) WITH STATUS 0 IN 1208.42 SECONDS
stats: 3340 7 1208.42 0

Solver Data

c Parsing PB file...
c Converting 721 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): sssssssss.s.ssss.ssss.ssssss.ssss..ssss..s.ssssssss.s.s.s.s.s.sss.sssss.ss.s.ss.s.ss.sssssssssssss.ssss.ssssssss.s.sssss.sss.ss.s.ss.sssssssssssssssssssssssssssssssssssssssssssss..sssssssssssssssssssss.sssss.sssssssss.ss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..sss.sssssssss.ssss.ssssssssssssss.ssssssssss.s.s.ssssssssssss.ss.ss.ss
c ---[1049]---> Adder-cost: 34840   maxlim: 2191589247   bits: 32/32
c ---[1048]---> BDD-cost:   37
c ---[1047]---> BDD-cost:   31
c ---[1046]---> BDD-cost:   35
c ---[1045]---> BDD-cost:   27
c ---[1044]---> BDD-cost:   37
c ---[1043]---> BDD-cost:   29
c ---[1042]---> BDD-cost:   29
c ---[1041]---> BDD-cost:   29
c ---[1040]---> BDD-cost:   29
c ---[1039]---> BDD-cost:   27
c ---[1038]---> BDD-cost:   27
c ---[1037]---> BDD-cost:   33
c ---[1036]---> BDD-cost:   27
c ---[1035]---> BDD-cost:   27
c ---[1034]---> BDD-cost:   27
c ---[1033]---> BDD-cost:   27
c ---[1032]---> BDD-cost:   37
c ---[1031]---> BDD-cost:   37
c ---[1030]---> BDD-cost:   37
c ---[1029]---> BDD-cost:   35
c ---[1028]---> BDD-cost:   37
c ---[1027]---> BDD-cost:   35
c ---[1026]---> BDD-cost:   31
c ---[1025]---> BDD-cost:   35
c ---[1024]---> BDD-cost:   31
c ---[1023]---> BDD-cost:   33
c ---[1022]---> BDD-cost:   27
c ---[1021]---> BDD-cost:   31
c ---[1020]---> BDD-cost:   27
c ---[1019]---> BDD-cost:   33
c ---[1018]---> BDD-cost:   37
c ---[1017]---> BDD-cost:   37
c ---[1016]---> BDD-cost:   37
c ---[1015]---> BDD-cost:   33
c ---[1014]---> BDD-cost:   35
c ---[1013]---> BDD-cost:   33
c ---[1012]---> BDD-cost:   33
c ---[1011]---> BDD-cost:   27
c ---[1010]---> BDD-cost:   31
c ---[1009]---> BDD-cost:   29
c ---[1008]---> BDD-cost:   35
c ---[1007]---> BDD-cost:   35
c ---[1006]---> BDD-cost:   33
c ---[1005]---> BDD-cost:   33
c ---[1004]---> BDD-cost:   31
c ---[1003]---> BDD-cost:   27
c ---[1002]---> BDD-cost:   27
c ---[1001]---> BDD-cost:   27
c ---[1000]---> BDD-cost:   37
c ---[ 999]---> BDD-cost:   37
c ---[ 998]---> BDD-cost:   35
c ---[ 997]---> BDD-cost:   35
c ---[ 996]---> BDD-cost:   31
c ---[ 995]---> BDD-cost:   33
c ---[ 994]---> BDD-cost:   31
c ---[ 993]---> BDD-cost:   31
c ---[ 992]---> BDD-cost:   27
c ---[ 991]---> BDD-cost:   31
c ---[ 990]---> BDD-cost:   37
c ---[ 989]---> BDD-cost:   33
c ---[ 988]---> BDD-cost:   33
c ---[ 987]---> BDD-cost:   27
c ---[ 986]---> BDD-cost:   31
c ---[ 985]---> BDD-cost:   27
c ---[ 984]---> BDD-cost:   27
c ---[ 983]---> BDD-cost:   37
c ---[ 982]---> BDD-cost:   27
c ---[ 981]---> BDD-cost:   37
c ---[ 980]---> BDD-cost:   35
c ---[ 979]---> BDD-cost:   37
c ---[ 978]---> BDD-cost:   31
c ---[ 977]---> BDD-cost:   35
c ---[ 976]---> BDD-cost:   31
c ---[ 975]---> BDD-cost:   29
c ---[ 974]---> BDD-cost:   37
c ---[ 973]---> BDD-cost:   33
c ---[ 972]---> BDD-cost:   37
c ---[ 971]---> BDD-cost:   27
c ---[ 970]---> BDD-cost:   35
c ---[ 969]---> BDD-cost:   37
c ---[ 968]---> BDD-cost:   33
c ---[ 967]---> BDD-cost:   37
c ---[ 966]---> BDD-cost:   33
c ---[ 965]---> BDD-cost:   37
c ---[ 964]---> BDD-cost:   35
c ---[ 963]---> BDD-cost:   37
c ---[ 962]---> BDD-cost:   31
c ---[ 961]---> BDD-cost:   37
c ---[ 960]---> BDD-cost:   31
c ---[ 959]---> BDD-cost:   33
c ---[ 958]---> BDD-cost:   37
c ---[ 957]---> BDD-cost:   33
c ---[ 956]---> BDD-cost:   37
c ---[ 955]---> BDD-cost:   37
c ---[ 954]---> BDD-cost:   37
c ---[ 953]---> BDD-cost:   35
c ---[ 952]---> BDD-cost:   37
c ---[ 951]---> BDD-cost:   37
c ---[ 950]---> BDD-cost:   35
c ---[ 949]---> BDD-cost:   35
c ---[ 948]---> BDD-cost:   33
c ---[ 947]---> BDD-cost:   33
c ---[ 946]---> BDD-cost:   33
c ---[ 945]---> BDD-cost:   31
c ---[ 944]---> BDD-cost:   37
c ---[ 943]---> BDD-cost:   37
c ---[ 942]---> BDD-cost:   37
c ---[ 941]---> BDD-cost:   37
c ---[ 940]---> BDD-cost:   35
c ---[ 939]---> BDD-cost:   37
c ---[ 938]---> BDD-cost:   35
c ---[ 937]---> BDD-cost:   35
c ---[ 936]---> BDD-cost:   37
c ---[ 935]---> BDD-cost:   33
c ---[ 934]---> BDD-cost:   33
c ---[ 933]---> BDD-cost:   33
c ---[ 932]---> BDD-cost:   33
c ---[ 931]---> BDD-cost:   33
c ---[ 930]---> BDD-cost:   31
c ---[ 929]---> BDD-cost:   35
c ---[ 928]---> BDD-cost:   37
c ---[ 927]---> BDD-cost:   35
c ---[ 926]---> BDD-cost:   37
c ---[ 925]---> BDD-cost:   37
c ---[ 924]---> BDD-cost:   37
c ---[ 923]---> BDD-cost:   35
c ---[ 922]---> BDD-cost:   35
c ---[ 921]---> BDD-cost:   37
c ---[ 920]---> BDD-cost:   37
c ---[ 919]---> BDD-cost:   33
c ---[ 918]---> BDD-cost:   37
c ---[ 917]---> BDD-cost:   37
c ---[ 916]---> BDD-cost:   37
c ---[ 915]---> BDD-cost:   37
c ---[ 914]---> BDD-cost:   37
c ---[ 913]---> BDD-cost:   35
c ---[ 912]---> BDD-cost:   37
c ---[ 911]---> BDD-cost:   37
c ---[ 910]---> BDD-cost:   37
c ---[ 909]---> BDD-cost:   35
c ---[ 908]---> BDD-cost:   33
c ---[ 907]---> BDD-cost:   37
c ---[ 906]---> BDD-cost:   37
c ---[ 905]---> BDD-cost:   35
c ---[ 904]---> BDD-cost:   35
c ---[ 903]---> BDD-cost:   37
c ---[ 902]---> BDD-cost:   35
c ---[ 901]---> BDD-cost:   35
c ---[ 900]---> BDD-cost:   35
c ---[ 899]---> BDD-cost:   33
c ---[ 898]---> BDD-cost:   35
c ---[ 897]---> BDD-cost:   35
c ---[ 896]---> BDD-cost:   35
c ---[ 895]---> BDD-cost:   35
c ---[ 894]---> BDD-cost:   33
c ---[ 893]---> BDD-cost:   37
c ---[ 892]---> BDD-cost:   33
c ---[ 891]---> BDD-cost:   33
c ---[ 890]---> BDD-cost:   31
c ---[ 889]---> BDD-cost:   33
c ---[ 888]---> BDD-cost:   33
c ---[ 887]---> BDD-cost:   37
c ---[ 886]---> BDD-cost:   31
c ---[ 885]---> BDD-cost:   33
c ---[ 884]---> BDD-cost:   33
c ---[ 883]---> BDD-cost:   33
c ---[ 882]---> BDD-cost:   33
c ---[ 881]---> BDD-cost:   31
c ---[ 880]---> BDD-cost:   33
c ---[ 879]---> BDD-cost:   31
c ---[ 878]---> BDD-cost:   31
c ---[ 877]---> BDD-cost:   31
c ---[ 876]---> BDD-cost:   29
c ---[ 875]---> BDD-cost:   31
c ---[ 874]---> BDD-cost:   37
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   37
c ---[ 871]---> BDD-cost:   33
c ---[ 870]---> BDD-cost:   35
c ---[ 869]---> BDD-cost:   33
c ---[ 868]---> BDD-cost:   35
c ---[ 867]---> BDD-cost:   37
c ---[ 866]---> BDD-cost:   35
c ---[ 865]---> BDD-cost:   35
c ---[ 864]---> BDD-cost:   33
c ---[ 863]---> BDD-cost:   29
c ---[ 862]---> BDD-cost:   37
c ---[ 861]---> BDD-cost:   37
c ---[ 860]---> BDD-cost:   35
c ---[ 859]---> BDD-cost:   35
c ---[ 858]---> BDD-cost:   33
c ---[ 857]---> BDD-cost:   33
c ---[ 856]---> BDD-cost:   31
c ---[ 855]---> BDD-cost:   27
c ---[ 854]---> BDD-cost:   37
c ---[ 853]---> BDD-cost:   37
c ---[ 852]---> BDD-cost:   35
c ---[ 851]---> BDD-cost:   31
c ---[ 850]---> BDD-cost:   33
c ---[ 849]---> BDD-cost:   37
c ---[ 848]---> BDD-cost:   37
c ---[ 847]---> BDD-cost:   35
c ---[ 846]---> BDD-cost:   33
c ---[ 845]---> BDD-cost:   37
c ---[ 844]---> BDD-cost:   31
c ---[ 843]---> BDD-cost:   37
c ---[ 842]---> BDD-cost:   29
c ---[ 841]---> BDD-cost:   27
c ---[ 840]---> BDD-cost:   27
c ---[ 839]---> BDD-cost:   37
c ---[ 838]---> BDD-cost:   31
c ---[ 837]---> BDD-cost:   37
c ---[ 836]---> BDD-cost:   35
c ---[ 835]---> BDD-cost:   37
c ---[ 834]---> BDD-cost:   35
c ---[ 833]---> BDD-cost:   33
c ---[ 832]---> BDD-cost:   33
c ---[ 831]---> BDD-cost:   35
c ---[ 830]---> BDD-cost:   35
c ---[ 829]---> BDD-cost:   33
c ---[ 828]---> BDD-cost:   37
c ---[ 827]---> BDD-cost:   37
c ---[ 826]---> BDD-cost:   27
c ---[ 825]---> BDD-cost:   35
c ---[ 824]---> BDD-cost:   35
c ---[ 823]---> BDD-cost:   35
c ---[ 822]---> BDD-cost:   37
c ---[ 821]---> BDD-cost:   37
c ---[ 820]---> BDD-cost:   37
c ---[ 819]---> BDD-cost:   35
c ---[ 818]---> BDD-cost:   35
c ---[ 817]---> BDD-cost:   37
c ---[ 816]---> BDD-cost:   37
c ---[ 815]---> BDD-cost:   31
c ---[ 814]---> BDD-cost:   37
c ---[ 813]---> BDD-cost:   35
c ---[ 812]---> BDD-cost:   35
c ---[ 811]---> BDD-cost:   35
c ---[ 810]---> BDD-cost:   33
c ---[ 809]---> BDD-cost:   33
c ---[ 808]---> BDD-cost:   33
c ---[ 807]---> BDD-cost:   33
c ---[ 806]---> BDD-cost:   33
c ---[ 805]---> BDD-cost:   31
c ---[ 804]---> BDD-cost:   29
c ---[ 803]---> BDD-cost:   37
c ---[ 802]---> BDD-cost:   37
c ---[ 801]---> BDD-cost:   33
c ---[ 800]---> BDD-cost:   37
c ---[ 799]---> BDD-cost:   37
c ---[ 798]---> BDD-cost:   37
c ---[ 797]---> BDD-cost:   33
c ---[ 796]---> BDD-cost:   31
c ---[ 795]---> BDD-cost:   35
c ---[ 794]---> BDD-cost:   33
c ---[ 793]---> BDD-cost:   31
c ---[ 792]---> BDD-cost:   37
c ---[ 791]---> BDD-cost:   37
c ---[ 790]---> BDD-cost:   37
c ---[ 783]---> BDD-cost:   27
c ---[ 772]---> BDD-cost:   27
c ---[ 761]---> BDD-cost:   29
c ---[ 750]---> BDD-cost:   33
c ---[ 739]---> BDD-cost:   37
c ---[ 728]---> BDD-cost:   35
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   33
c ---[ 705]---> BDD-cost:   33
c ---[ 694]---> BDD-cost:   33
c ---[ 683]---> BDD-cost:   33
c ---[ 672]---> BDD-cost:   33
c ---[ 661]---> BDD-cost:   33
c ---[ 650]---> BDD-cost:   31
c ---[ 639]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 608]---> BDD-cost:   35
c ---[ 607]---> BDD-cost:   37
c ---[ 600]---> Adder-cost: 1983   maxlim: 44   bits: 7/6
c ---[ 599]---> Adder-cost: 1199   maxlim: 36   bits: 7/6
c ---[ 598]---> Adder-cost: 1144   maxlim: 36   bits: 7/6
c ---[ 597]---> BDD-cost:   35
c ---[ 587]---> BDD-cost:   33
c ---[ 582]---> Adder-cost: 2030   maxlim: 37   bits: 7/6
c ---[ 581]---> Adder-cost: 1403   maxlim: 32   bits: 7/6
c ---[ 576]---> BDD-cost:   37
c ---[ 567]---> BDD-cost:   33
c ---[ 556]---> BDD-cost:   27
c ---[ 546]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   35
c ---[ 525]---> BDD-cost:   33
c ---[ 514]---> BDD-cost:   35
c ---[ 503]---> BDD-cost:   33
c ---[ 502]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   33
c ---[ 482]---> BDD-cost:   33
c ---[ 472]---> BDD-cost:   31
c ---[ 462]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   35
c ---[ 440]---> BDD-cost:   37
c ---[ 429]---> BDD-cost:   33
c ---[ 418]---> BDD-cost:   33
c ---[ 407]---> BDD-cost:   31
c ---[ 396]---> BDD-cost:   33
c ---[ 395]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   33
c ---[ 373]---> BDD-cost:   31
c ---[ 363]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   37
c ---[ 355]---> BDD-cost:   37
c ---[ 354]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   35
c ---[ 352]---> BDD-cost:   35
c ---[ 351]---> BDD-cost:   33
c ---[ 350]---> BDD-cost:   35
c ---[ 349]---> BDD-cost:   31
c ---[ 348]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   33
c ---[ 346]---> BDD-cost:   33
c ---[ 345]---> BDD-cost:   33
c ---[ 344]---> BDD-cost:   31
c ---[ 343]---> BDD-cost:   27
c ---[ 342]---> BDD-cost:   33
c ---[ 341]---> BDD-cost:   31
c ---[ 340]---> BDD-cost:   33
c ---[ 339]---> BDD-cost:   37
c ---[ 338]---> BDD-cost:   33
c ---[ 337]---> BDD-cost:   33
c ---[ 336]---> BDD-cost:   31
c ---[ 335]---> BDD-cost:   33
c ---[ 334]---> BDD-cost:   31
c ---[ 333]---> BDD-cost:   27
c ---[ 332]---> BDD-cost:   31
c ---[ 331]---> BDD-cost:   29
c ---[ 330]---> BDD-cost:   31
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   34
c ---[ 327]---> BDD-cost: 1577
c ---[ 326]---> Adder-cost: 1245   maxlim: 13   bits: 5/4
c ---[ 325]---> BDD-cost: 2212
c ---[ 324]---> Adder-cost: 791   maxlim: 11   bits: 5/4
c ---[ 323]---> BDD-cost:  930
c ---[ 322]---> Adder-cost: 622   maxlim: 14   bits: 5/4
c ---[ 321]---> Adder-cost: 342   maxlim: 10   bits: 5/4
c ---[ 320]---> Adder-cost: 366   maxlim: 13   bits: 5/4
c ---[ 319]---> BDD-cost:   36
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> Adder-cost: 375   maxlim: 12   bits: 5/4
c ---[ 316]---> BDD-cost:  816
c ---[ 315]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 314]---> BDD-cost:    1
c ---[ 313]---> Adder-cost: 259   maxlim: 13   bits: 5/4
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 310]---> BDD-cost:  817
c ---[ 309]---> BDD-cost:   51
c ---[ 308]---> BDD-cost:  253
c ---[ 307]---> Adder-cost: 426   maxlim: 10   bits: 5/4
c ---[ 306]---> BDD-cost:  565
c ---[ 305]---> BDD-cost:  802
c ---[ 304]---> BDD-cost:  164
c ---[ 303]---> BDD-cost:   72
c ---[ 302]---> BDD-cost:   93
c ---[ 301]---> Adder-cost: 772   maxlim: 14   bits: 5/4
c ---[ 300]---> Adder-cost: 287   maxlim: 12   bits: 5/4
c ---[ 299]---> BDD-cost:  157
c ---[ 298]---> BDD-cost:  249
c ---[ 297]---> Adder-cost: 472   maxlim: 15   bits: 5/4
c ---[ 296]---> Adder-cost: 203   maxlim: 12   bits: 5/4
c ---[ 295]---> BDD-cost:    2
c ---[ 294]---> BDD-cost:  906
c ---[ 293]---> BDD-cost:   62
c ---[ 292]---> BDD-cost:  167
c ---[ 291]---> BDD-cost:    4
c ---[ 290]---> BDD-cost:   20
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    2
c ---[ 286]---> BDD-cost:    8
c ---[ 285]---> BDD-cost:  147
c ---[ 284]---> BDD-cost:  745
c ---[ 283]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:   24
c ---[ 279]---> BDD-cost:   54
c ---[ 278]---> Adder-cost: 1107   maxlim: 10   bits: 5/4
c ---[ 277]---> BDD-cost:   32
c ---[ 276]---> BDD-cost:  879
c ---[ 275]---> Adder-cost: 1319   maxlim: 13   bits: 5/4
c ---[ 274]---> BDD-cost: 2088
c ---[ 273]---> Adder-cost: 2987   maxlim: 17   bits: 6/5
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost: 2736
c ---[ 270]---> Adder-cost: 2558   maxlim: 19   bits: 6/5
c ---[ 269]---> BDD-cost:  492
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> Adder-cost: 738   maxlim: 16   bits: 6/5
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:   72
c ---[ 264]---> BDD-cost:  100
c ---[ 263]---> Adder-cost: 995   maxlim: 19   bits: 6/5
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    2
c ---[ 260]---> Adder-cost: 463   maxlim: 18   bits: 6/5
c ---[ 259]---> BDD-cost:  767
c ---[ 258]---> Adder-cost: 912   maxlim: 9   bits: 5/4
c ---[ 257]---> Adder-cost: 1537   maxlim: 21   bits: 6/5
c ---[ 256]---> BDD-cost:  889
c ---[ 255]---> Adder-cost: 1017   maxlim: 17   bits: 6/5
c ---[ 254]---> Adder-cost: 569   maxlim: 9   bits: 5/4
c ---[ 253]---> BDD-cost: 1704
c ---[ 252]---> Adder-cost: 369   maxlim: 19   bits: 6/5
c ---[ 251]---> BDD-cost:  932
c ---[ 250]---> Adder-cost: 1316   maxlim: 24   bits: 6/5
c ---[ 249]---> BDD-cost: 1516
c ---[ 248]---> Adder-cost: 1518   maxlim: 17   bits: 6/5
c ---[ 247]---> BDD-cost:  242
c ---[ 246]---> Adder-cost: 319   maxlim: 24   bits: 6/5
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> Adder-cost: 726   maxlim: 20   bits: 6/5
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> Adder-cost: 659   maxlim: 17   bits: 6/5
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:  497
c ---[ 239]---> Adder-cost: 423   maxlim: 16   bits: 6/5
c ---[ 238]---> BDD-cost:  151
c ---[ 237]---> BDD-cost:  101
c ---[ 236]---> Adder-cost: 941   maxlim: 14   bits: 5/4
c ---[ 235]---> BDD-cost:   46
c ---[ 234]---> Adder-cost: 705   maxlim: 11   bits: 5/4
c ---[ 233]---> BDD-cost:   70
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> Adder-cost: 150   maxlim: 11   bits: 5/4
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:   79
c ---[ 226]---> Adder-cost: 524   maxlim: 17   bits: 6/5
c ---[ 225]---> Adder-cost: 606   maxlim: 21   bits: 6/5
c ---[ 224]---> BDD-cost:   32
c ---[ 223]---> Adder-cost: 1071   maxlim: 14   bits: 5/4
c ---[ 222]---> BDD-cost:   24
c ---[ 221]---> BDD-cost: 1540
c ---[ 220]---> BDD-cost: 2152
c ---[ 219]---> BDD-cost:  115
c ---[ 218]---> BDD-cost: 1715
c ---[ 217]---> Adder-cost: 1890   maxlim: 23   bits: 6/5
c ---[ 216]---> BDD-cost:  135
c ---[ 215]---> Adder-cost: 927   maxlim: 19   bits: 6/5
c ---[ 214]---> BDD-cost: 1261
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> Adder-cost: 221   maxlim: 23   bits: 6/5
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> Adder-cost: 760   maxlim: 20   bits: 6/5
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:  382
c ---[ 206]---> BDD-cost:  656
c ---[ 205]---> Adder-cost: 1489   maxlim: 16   bits: 6/5
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:  308
c ---[ 202]---> Adder-cost: 502   maxlim: 12   bits: 5/4
c ---[ 201]---> Adder-cost: 967   maxlim: 10   bits: 5/4
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:    1
c ---[ 198]---> Adder-cost: 862   maxlim: 13   bits: 5/4
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> Adder-cost: 300   maxlim: 13   bits: 5/4
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:   68
c ---[ 192]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 191]---> Adder-cost: 708   maxlim: 28   bits: 6/5
c ---[ 190]---> BDD-cost:  156
c ---[ 189]---> Adder-cost: 566   maxlim: 10   bits: 5/4
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   37
c ---[ 183]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 182]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 181]---> BDD-cost:   32
c ---[ 180]---> Adder-cost: 816   maxlim: 16   bits: 6/5
c ---[ 179]---> Adder-cost: 968   maxlim: 20   bits: 6/5
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> Adder-cost: 789   maxlim: 17   bits: 6/5
c ---[ 176]---> Adder-cost: 535   maxlim: 16   bits: 6/5
c ---[ 175]---> Adder-cost: 615   maxlim: 20   bits: 6/5
c ---[ 174]---> BDD-cost:   18
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> Adder-cost: 572   maxlim: 17   bits: 6/5
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 169]---> Adder-cost: 256   maxlim: 22   bits: 6/5
c ---[ 168]---> Adder-cost: 546   maxlim: 20   bits: 6/5
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> Adder-cost: 221   maxlim: 23   bits: 6/5
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> Adder-cost: 326   maxlim: 20   bits: 6/5
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> Adder-cost: 1639   maxlim: 15   bits: 5/4
c ---[ 160]---> Adder-cost: 936   maxlim: 13   bits: 5/4
c ---[ 159]---> BDD-cost:   64
c ---[ 158]---> BDD-cost:  250
c ---[ 157]---> Adder-cost: 579   maxlim: 9   bits: 5/4
c ---[ 156]---> BDD-cost:  769
c ---[ 155]---> BDD-cost:   37
c ---[ 154]---> BDD-cost:  977
c ---[ 153]---> BDD-cost:  171
c ---[ 152]---> BDD-cost:   40
c ---[ 151]---> BDD-cost:  250
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[ 148]---> BDD-cost:   32
c ---[ 147]---> BDD-cost:   88
c ---[ 146]---> BDD-cost:  491
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:  375
c ---[ 143]---> BDD-cost:  471
c ---[ 142]---> Adder-cost: 2563   maxlim: 22   bits: 6/5
c ---[ 141]---> Adder-cost: 1127   maxlim: 12   bits: 5/4
c ---[ 140]---> Adder-cost: 1321   maxlim: 12   bits: 5/4
c ---[ 139]---> BDD-cost:  326
c ---[ 138]---> Adder-cost: 752   maxlim: 12   bits: 5/4
c ---[ 137]---> BDD-cost:  394
c ---[ 136]---> Adder-cost: 1087   maxlim: 12   bits: 5/4
c ---[ 135]---> BDD-cost:  232
c ---[ 134]---> BDD-cost: 1615
c ---[ 133]---> Adder-cost: 2295   maxlim: 19   bits: 6/5
c ---[ 132]---> BDD-cost: 2419
c ---[ 131]---> Adder-cost: 1457   maxlim: 17   bits: 6/5
c ---[ 130]---> BDD-cost: 1026
c ---[ 129]---> BDD-cost: 1706
c ---[ 128]---> BDD-cost:  242
c ---[ 127]---> Adder-cost: 1319   maxlim: 14   bits: 5/4
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> Adder-cost: 508   maxlim: 22   bits: 6/5
c ---[ 123]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 122]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> Adder-cost: 570   maxlim: 21   bits: 6/5
c ---[ 114]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 113]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 108]---> Adder-cost: 544   maxlim: 10   bits: 5/4
c ---[ 107]---> BDD-cost:   65
c ---[ 106]---> BDD-cost:  871
c ---[ 105]---> BDD-cost: 1115
c ---[ 104]---> BDD-cost:   32
c ---[ 103]---> BDD-cost:   25
c ---[ 102]---> Adder-cost: 821   maxlim: 10   bits: 5/4
c ---[ 101]---> BDD-cost:  107
c ---[ 100]---> Adder-cost: 505   maxlim: 9   bits: 5/4
c ---[  99]---> Adder-cost: 1037   maxlim: 20   bits: 6/5
c ---[  98]---> Adder-cost: 280   maxlim: 10   bits: 5/4
c ---[  97]---> Adder-cost: 363   maxlim: 10   bits: 5/4
c ---[  96]---> Adder-cost: 717   maxlim: 19   bits: 6/5
c ---[  95]---> BDD-cost:  795
c ---[  94]---> Adder-cost: 565   maxlim: 14   bits: 5/4
c ---[  93]---> BDD-cost:   65
c ---[  92]---> BDD-cost:  102
c ---[  91]---> Adder-cost: 444   maxlim: 21   bits: 6/5
c ---[  90]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[  89]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[  88]---> BDD-cost:   78
c ---[  87]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[  86]---> BDD-cost:   90
c ---[  85]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[  84]---> BDD-cost:    1
c ---[  83]---> Adder-cost: 861   maxlim: 15   bits: 5/4
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost: 1376
c ---[  80]---> Adder-cost: 792   maxlim: 19   bits: 6/5
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:  688
c ---[  77]---> Adder-cost: 314   maxlim: 20   bits: 6/5
c ---[  76]---> BDD-cost:   96
c ---[  75]---> BDD-cost:    1
c ---[  74]---> Adder-cost: 314   maxlim: 20   bits: 6/5
c ---[  73]---> BDD-cost:  161
c ---[  72]---> BDD-cost:  170
c ---[  71]---> Adder-cost: 490   maxlim: 18   bits: 6/5
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> Adder-cost: 210   maxlim: 19   bits: 6/5
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> Adder-cost: 302   maxlim: 18   bits: 6/5
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> Adder-cost: 357   maxlim: 11   bits: 5/4
c ---[  60]---> BDD-cost:   30
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  56]---> BDD-cost:   72
c ---[  55]---> BDD-cost:   75
c ---[  54]---> BDD-cost:  302
c ---[  53]---> BDD-cost:  303
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:   46
c ---[  50]---> BDD-cost:  532
c ---[  49]---> Adder-cost: 474   maxlim: 10   bits: 5/4
c ---[  48]---> Adder-cost: 801   maxlim: 22   bits: 6/5
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   86
c ---[  45]---> BDD-cost:  971
c ---[  44]---> Adder-cost: 1446   maxlim: 21   bits: 6/5
c ---[  43]---> BDD-cost:  173
c ---[  42]---> Adder-cost: 685   maxlim: 10   bits: 5/4
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:  170
c ---[  39]---> Adder-cost: 732   maxlim: 19   bits: 6/5
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> Adder-cost: 216   maxlim: 19   bits: 6/5
c ---[  35]---> BDD-cost:   78
c ---[  34]---> BDD-cost:   98
c ---[  33]---> Adder-cost: 216   maxlim: 19   bits: 6/5
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> Adder-cost: 578   maxlim: 17   bits: 6/5
c ---[  29]---> BDD-cost:    1
c ---[  28]---> Adder-cost: 640   maxlim: 16   bits: 6/5
c ---[  27]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   92
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   22
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  13]---> BDD-cost:  182
c ---[  12]---> Adder-cost: 367   maxlim: 12   bits: 5/4
c ---[  11]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   35
c ---[   9]---> BDD-cost:  505
c ---[   8]---> Adder-cost: 747   maxlim: 15   bits: 5/4
c ---[   7]---> BDD-cost:    1
c ---[   6]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:  794
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:  132
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  857159  3090424 |  285719       0        0     nan |  0.000 % |
c |       100 |  857159  3090424 |  314290     100      396     4.0 |  0.831 % |
c |       250 |  857159  3090424 |  345719     250      961     3.8 |  0.831 % |
c |       475 |  857142  3090361 |  380291     471     2102     4.5 |  0.832 % |
c |       812 |  857142  3090361 |  418321     808     4261     5.3 |  0.832 % |
c |      1318 |  857142  3090361 |  460153    1314     7647     5.8 |  0.832 % |
c |      2078 |  857063  3090064 |  506168    2070    14365     6.9 |  0.833 % |
c |      3217 |  857003  3089858 |  556785    3203    26997     8.4 |  0.840 % |
c |      4925 |  855671  3085081 |  612464    4709    51644    11.0 |  0.968 % |
c |      7487 |  854820  3082024 |  673710    7156    67857     9.5 |  1.046 % |
c |     11333 |  854812  3081994 |  741081   11001   107422     9.8 |  1.046 % |
c |     17100 |  854467  3080725 |  815189   16737   165968     9.9 |  1.061 % |
c |     25749 |  853831  3078415 |  896708   25301   245089     9.7 |  1.105 % |
c |     38723 |  851689  3070565 |  986379   38006   387465    10.2 |  1.274 % |
c |     58185 |  847988  3057700 | 1085017   56909   758550    13.3 |  1.626 % |
c |     87378 |  847914  3057432 | 1193519   86092  2910169    33.8 |  1.630 % |
c |    131168 |  844266  3044674 | 1312871  129479  3855943    29.8 |  1.919 % |

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/28119/stat): 28119 (minisat+_script) R 28118 28119 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855507747 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28119/statm): 174 3 169 147 0 27 0
[pid=28119] 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=28120
New process pid=28121
New process pid=28122
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
One traced child (pid=28121) 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=28122) exited with status: 0
One traced child (pid=28120) exited with status: 0
New process pid=28123
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-nsrand-ipx.opb

[startup+10.0033 s]
Raw data (loadavg): 1.12 1.03 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 7823 0 0 0 938 29 0 0 25 0 1 0 1855507752 23388160 5135 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 5710 5135 145 145 0 5565 0
[pid=28123] vsize: 22840
Current children cumulated CPU time (s) 9.69
Current children cumulated vsize (Kb) 24964

[startup+20.0042 s]
Raw data (loadavg): 1.10 1.03 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 11911 0 0 0 1924 40 0 0 25 0 1 0 1855507752 23404544 5140 4294967295 134512640 135094434 3221224432 3221220280 134676461 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 5714 5140 145 145 0 5569 0
[pid=28123] vsize: 22856
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 24980

[startup+30.0051 s]
Raw data (loadavg): 1.08 1.03 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 16065 0 0 0 2907 51 0 0 25 0 1 0 1855507752 22994944 5052 4294967295 134512640 135094434 3221224432 3221221516 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 5614 5052 145 145 0 5469 0
[pid=28123] vsize: 22456
Current children cumulated CPU time (s) 29.6
Current children cumulated vsize (Kb) 24580

[startup+40.0051 s]
Raw data (loadavg): 1.07 1.03 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 20340 0 0 0 3895 60 0 0 25 0 1 0 1855507752 22929408 5039 4294967295 134512640 135094434 3221224432 3221221792 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 5598 5039 145 145 0 5453 0
[pid=28123] vsize: 22392
Current children cumulated CPU time (s) 39.57
Current children cumulated vsize (Kb) 24516

[startup+50.006 s]
Raw data (loadavg): 1.06 1.03 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 32800 0 0 0 4832 97 0 0 25 0 1 0 1855507752 62001152 14487 4294967295 134512640 135094434 3221224432 3221223188 134596388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 15137 14487 145 145 0 14992 0
[pid=28123] vsize: 60548
Current children cumulated CPU time (s) 49.31
Current children cumulated vsize (Kb) 62672

[startup+60.0069 s]
Raw data (loadavg): 1.05 1.02 0.94 1/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) T 28119 28119 31027 0 -1 0 38502 0 0 0 5790 118 0 0 22 0 1 0 1855507752 87498752 20164 4294967295 134512640 135094434 3221224432 3221220252 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28123/statm): 21362 20164 145 145 0 21217 0
[pid=28123] vsize: 85448
Current children cumulated CPU time (s) 59.1
Current children cumulated vsize (Kb) 87572

[startup+70.0089 s]
Raw data (loadavg): 1.04 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44385 0 0 0 6734 146 0 0 25 0 1 0 1855507752 114040832 26047 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 27842 26047 145 145 0 27697 0
[pid=28123] vsize: 111368
Current children cumulated CPU time (s) 68.82
Current children cumulated vsize (Kb) 113492

[startup+80.0098 s]
Raw data (loadavg): 1.04 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44481 0 0 0 7731 148 0 0 25 0 1 0 1855507752 114438144 26143 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 27939 26143 145 145 0 27794 0
[pid=28123] vsize: 111756
Current children cumulated CPU time (s) 78.81
Current children cumulated vsize (Kb) 113880

[startup+90.0107 s]
Raw data (loadavg): 1.03 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44495 0 0 0 8730 148 0 0 25 0 1 0 1855507752 114495488 26157 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 27953 26157 145 145 0 27808 0
[pid=28123] vsize: 111812
Current children cumulated CPU time (s) 88.8
Current children cumulated vsize (Kb) 113936

[startup+100.012 s]
Raw data (loadavg): 1.02 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44524 0 0 0 9730 149 0 0 25 0 1 0 1855507752 114614272 26186 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 27982 26186 145 145 0 27837 0
[pid=28123] vsize: 111928
Current children cumulated CPU time (s) 98.81
Current children cumulated vsize (Kb) 114052

[startup+110.013 s]
Raw data (loadavg): 1.02 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44653 0 0 0 10728 150 0 0 25 0 1 0 1855507752 115142656 26315 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28111 26315 145 145 0 27966 0
[pid=28123] vsize: 112444
Current children cumulated CPU time (s) 108.8
Current children cumulated vsize (Kb) 114568

[startup+120.014 s]
Raw data (loadavg): 1.02 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44735 0 0 0 11726 151 0 0 25 0 1 0 1855507752 115470336 26397 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28191 26397 145 145 0 28046 0
[pid=28123] vsize: 112764
Current children cumulated CPU time (s) 118.79
Current children cumulated vsize (Kb) 114888

[startup+130.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44823 0 0 0 12724 152 0 0 25 0 1 0 1855507752 115855360 26485 4294967295 134512640 135094434 3221224432 3221223044 134563104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28285 26485 145 145 0 28140 0
[pid=28123] vsize: 113140
Current children cumulated CPU time (s) 128.78
Current children cumulated vsize (Kb) 115264

[startup+140.015 s]
Raw data (loadavg): 1.01 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 44980 0 0 0 13721 154 0 0 25 0 1 0 1855507752 116486144 26642 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28439 26642 145 145 0 28294 0
[pid=28123] vsize: 113756
Current children cumulated CPU time (s) 138.77
Current children cumulated vsize (Kb) 115880

[startup+150.017 s]
Raw data (loadavg): 1.01 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45072 0 0 0 14719 155 0 0 25 0 1 0 1855507752 116854784 26734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28529 26734 145 145 0 28384 0
[pid=28123] vsize: 114116
Current children cumulated CPU time (s) 148.76
Current children cumulated vsize (Kb) 116240

[startup+160.018 s]
Raw data (loadavg): 1.01 1.02 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45111 0 0 0 15718 155 0 0 25 0 1 0 1855507752 117010432 26773 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28567 26773 145 145 0 28422 0
[pid=28123] vsize: 114268
Current children cumulated CPU time (s) 158.75
Current children cumulated vsize (Kb) 116392

[startup+170.019 s]
Raw data (loadavg): 1.01 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45139 0 0 0 16717 156 0 0 25 0 1 0 1855507752 117182464 26801 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28609 26801 145 145 0 28464 0
[pid=28123] vsize: 114436
Current children cumulated CPU time (s) 168.75
Current children cumulated vsize (Kb) 116560

[startup+180.02 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45196 0 0 0 17716 156 0 0 25 0 1 0 1855507752 117411840 26858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28665 26858 145 145 0 28520 0
[pid=28123] vsize: 114660
Current children cumulated CPU time (s) 178.74
Current children cumulated vsize (Kb) 116784

[startup+190.021 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45233 0 0 0 18716 157 0 0 25 0 1 0 1855507752 117555200 26895 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28700 26895 145 145 0 28555 0
[pid=28123] vsize: 114800
Current children cumulated CPU time (s) 188.75
Current children cumulated vsize (Kb) 116924

[startup+200.022 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45279 0 0 0 19714 158 0 0 25 0 1 0 1855507752 117735424 26941 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28744 26941 145 145 0 28599 0
[pid=28123] vsize: 114976
Current children cumulated CPU time (s) 198.74
Current children cumulated vsize (Kb) 117100

[startup+210.023 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45305 0 0 0 20713 158 0 0 25 0 1 0 1855507752 117837824 26967 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 28769 26967 145 145 0 28624 0
[pid=28123] vsize: 115076
Current children cumulated CPU time (s) 208.73
Current children cumulated vsize (Kb) 117200

[startup+220.025 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45328 0 0 0 21713 158 0 0 25 0 1 0 1855507752 117927936 26990 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28791 26990 145 145 0 28646 0
[pid=28123] vsize: 115164
Current children cumulated CPU time (s) 218.73
Current children cumulated vsize (Kb) 117288

[startup+230.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45349 0 0 0 22713 158 0 0 25 0 1 0 1855507752 118009856 27011 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28811 27011 145 145 0 28666 0
[pid=28123] vsize: 115244
Current children cumulated CPU time (s) 228.73
Current children cumulated vsize (Kb) 117368

[startup+240.026 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45364 0 0 0 23712 158 0 0 25 0 1 0 1855507752 118071296 27026 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28826 27026 145 145 0 28681 0
[pid=28123] vsize: 115304
Current children cumulated CPU time (s) 238.72
Current children cumulated vsize (Kb) 117428

[startup+250.027 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45374 0 0 0 24712 159 0 0 25 0 1 0 1855507752 118108160 27036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28835 27036 145 145 0 28690 0
[pid=28123] vsize: 115340
Current children cumulated CPU time (s) 248.73
Current children cumulated vsize (Kb) 117464

[startup+260.027 s]
Raw data (loadavg): 1.00 1.01 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45389 0 0 0 25712 159 0 0 25 0 1 0 1855507752 118165504 27051 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28849 27051 145 145 0 28704 0
[pid=28123] vsize: 115396
Current children cumulated CPU time (s) 258.73
Current children cumulated vsize (Kb) 117520

[startup+270.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45407 0 0 0 26712 159 0 0 25 0 1 0 1855507752 118239232 27069 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28867 27069 145 145 0 28722 0
[pid=28123] vsize: 115468
Current children cumulated CPU time (s) 268.73
Current children cumulated vsize (Kb) 117592

[startup+280.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45423 0 0 0 27712 159 0 0 25 0 1 0 1855507752 118300672 27085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28882 27085 145 145 0 28737 0
[pid=28123] vsize: 115528
Current children cumulated CPU time (s) 278.73
Current children cumulated vsize (Kb) 117652

[startup+290.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45441 0 0 0 28712 159 0 0 25 0 1 0 1855507752 118370304 27103 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28899 27103 145 145 0 28754 0
[pid=28123] vsize: 115596
Current children cumulated CPU time (s) 288.73
Current children cumulated vsize (Kb) 117720

[startup+300.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45451 0 0 0 29712 159 0 0 25 0 1 0 1855507752 118411264 27113 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28909 27113 145 145 0 28764 0
[pid=28123] vsize: 115636
Current children cumulated CPU time (s) 298.73
Current children cumulated vsize (Kb) 117760

[startup+310.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45464 0 0 0 30712 160 0 0 25 0 1 0 1855507752 118460416 27126 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28921 27126 145 145 0 28776 0
[pid=28123] vsize: 115684
Current children cumulated CPU time (s) 308.74
Current children cumulated vsize (Kb) 117808

[startup+320.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45474 0 0 0 31712 160 0 0 25 0 1 0 1855507752 118501376 27136 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28931 27136 145 145 0 28786 0
[pid=28123] vsize: 115724
Current children cumulated CPU time (s) 318.74
Current children cumulated vsize (Kb) 117848

[startup+330.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45489 0 0 0 32712 160 0 0 25 0 1 0 1855507752 118558720 27151 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28945 27151 145 145 0 28800 0
[pid=28123] vsize: 115780
Current children cumulated CPU time (s) 328.74
Current children cumulated vsize (Kb) 117904

[startup+340.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45501 0 0 0 33712 160 0 0 25 0 1 0 1855507752 118607872 27163 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 28957 27163 145 145 0 28812 0
[pid=28123] vsize: 115828
Current children cumulated CPU time (s) 338.74
Current children cumulated vsize (Kb) 117952

[startup+350.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45547 0 0 0 34712 160 0 0 25 0 1 0 1855507752 118919168 27209 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29033 27209 145 145 0 28888 0
[pid=28123] vsize: 116132
Current children cumulated CPU time (s) 348.74
Current children cumulated vsize (Kb) 118256

[startup+360.037 s]
Raw data (loadavg): 1.08 1.02 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45562 0 0 0 35712 160 0 0 25 0 1 0 1855507752 118976512 27224 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29047 27224 145 145 0 28902 0
[pid=28123] vsize: 116188
Current children cumulated CPU time (s) 358.74
Current children cumulated vsize (Kb) 118312

[startup+370.039 s]
Raw data (loadavg): 1.07 1.02 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45635 0 0 0 36711 161 0 0 25 0 1 0 1855507752 119263232 27297 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29117 27297 145 145 0 28972 0
[pid=28123] vsize: 116468
Current children cumulated CPU time (s) 368.74
Current children cumulated vsize (Kb) 118592

[startup+380.04 s]
Raw data (loadavg): 1.06 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45645 0 0 0 37711 161 0 0 25 0 1 0 1855507752 119304192 27307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29127 27307 145 145 0 28982 0
[pid=28123] vsize: 116508
Current children cumulated CPU time (s) 378.74
Current children cumulated vsize (Kb) 118632

[startup+390.04 s]
Raw data (loadavg): 1.05 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45654 0 0 0 38710 162 0 0 25 0 1 0 1855507752 119341056 27316 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29136 27316 145 145 0 28991 0
[pid=28123] vsize: 116544
Current children cumulated CPU time (s) 388.74
Current children cumulated vsize (Kb) 118668

[startup+400.041 s]
Raw data (loadavg): 1.04 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45664 0 0 0 39710 162 0 0 25 0 1 0 1855507752 119377920 27326 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29145 27326 145 145 0 29000 0
[pid=28123] vsize: 116580
Current children cumulated CPU time (s) 398.74
Current children cumulated vsize (Kb) 118704

[startup+410.042 s]
Raw data (loadavg): 1.03 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45668 0 0 0 40709 162 0 0 25 0 1 0 1855507752 119394304 27330 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29149 27330 145 145 0 29004 0
[pid=28123] vsize: 116596
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 118720

[startup+420.043 s]
Raw data (loadavg): 1.03 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45695 0 0 0 41709 162 0 0 25 0 1 0 1855507752 119496704 27357 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29174 27357 145 145 0 29029 0
[pid=28123] vsize: 116696
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 118820

[startup+430.045 s]
Raw data (loadavg): 1.02 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45696 0 0 0 42709 162 0 0 25 0 1 0 1855507752 119500800 27358 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29175 27358 145 145 0 29030 0
[pid=28123] vsize: 116700
Current children cumulated CPU time (s) 428.73
Current children cumulated vsize (Kb) 118824

[startup+440.045 s]
Raw data (loadavg): 1.02 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45706 0 0 0 43709 163 0 0 25 0 1 0 1855507752 119541760 27368 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29185 27368 145 145 0 29040 0
[pid=28123] vsize: 116740
Current children cumulated CPU time (s) 438.74
Current children cumulated vsize (Kb) 118864

[startup+450.046 s]
Raw data (loadavg): 1.02 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45744 0 0 0 44709 163 0 0 25 0 1 0 1855507752 119689216 27406 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29221 27406 145 145 0 29076 0
[pid=28123] vsize: 116884
Current children cumulated CPU time (s) 448.74
Current children cumulated vsize (Kb) 119008

[startup+460.047 s]
Raw data (loadavg): 1.01 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45770 0 0 0 45709 163 0 0 25 0 1 0 1855507752 119791616 27432 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29246 27432 145 145 0 29101 0
[pid=28123] vsize: 116984
Current children cumulated CPU time (s) 458.74
Current children cumulated vsize (Kb) 119108

[startup+470.048 s]
Raw data (loadavg): 1.01 1.01 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45808 0 0 0 46708 163 0 0 25 0 1 0 1855507752 119939072 27470 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29282 27470 145 145 0 29137 0
[pid=28123] vsize: 117128
Current children cumulated CPU time (s) 468.73
Current children cumulated vsize (Kb) 119252

[startup+480.049 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45825 0 0 0 47708 163 0 0 25 0 1 0 1855507752 120004608 27487 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29298 27487 145 145 0 29153 0
[pid=28123] vsize: 117192
Current children cumulated CPU time (s) 478.73
Current children cumulated vsize (Kb) 119316

[startup+490.05 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45840 0 0 0 48708 163 0 0 25 0 1 0 1855507752 120061952 27502 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29312 27502 145 145 0 29167 0
[pid=28123] vsize: 117248
Current children cumulated CPU time (s) 488.73
Current children cumulated vsize (Kb) 119372

[startup+500.051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45855 0 0 0 49708 163 0 0 25 0 1 0 1855507752 120123392 27517 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29327 27517 145 145 0 29182 0
[pid=28123] vsize: 117308
Current children cumulated CPU time (s) 498.73
Current children cumulated vsize (Kb) 119432

[startup+510.052 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45869 0 0 0 50708 163 0 0 25 0 1 0 1855507752 120176640 27531 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29340 27531 145 145 0 29195 0
[pid=28123] vsize: 117360
Current children cumulated CPU time (s) 508.73
Current children cumulated vsize (Kb) 119484

[startup+520.053 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 45874 0 0 0 51708 163 0 0 25 0 1 0 1855507752 120197120 27536 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29345 27536 145 145 0 29200 0
[pid=28123] vsize: 117380
Current children cumulated CPU time (s) 518.73
Current children cumulated vsize (Kb) 119504

[startup+530.053 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 46016 0 0 0 52707 164 0 0 25 0 1 0 1855507752 120762368 27678 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29483 27678 145 145 0 29338 0
[pid=28123] vsize: 117932
Current children cumulated CPU time (s) 528.73
Current children cumulated vsize (Kb) 120056

[startup+540.054 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 46462 0 0 0 53698 167 0 0 25 0 1 0 1855507752 122560512 28124 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 29922 28124 145 145 0 29777 0
[pid=28123] vsize: 119688
Current children cumulated CPU time (s) 538.67
Current children cumulated vsize (Kb) 121812

[startup+550.055 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 47090 0 0 0 54688 171 0 0 25 0 1 0 1855507752 125370368 28752 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 30608 28752 145 145 0 30463 0
[pid=28123] vsize: 122432
Current children cumulated CPU time (s) 548.61
Current children cumulated vsize (Kb) 124556

[startup+560.055 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 47587 0 0 0 55680 174 0 0 25 0 1 0 1855507752 127385600 29249 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 31100 29249 145 145 0 30955 0
[pid=28123] vsize: 124400
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 126524

[startup+570.056 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 48057 0 0 0 56673 177 0 0 25 0 1 0 1855507752 129331200 29719 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 31575 29719 145 145 0 31430 0
[pid=28123] vsize: 126300
Current children cumulated CPU time (s) 568.52
Current children cumulated vsize (Kb) 128424

[startup+580.057 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 48460 0 0 0 57666 180 0 0 25 0 1 0 1855507752 130965504 30122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 31974 30122 145 145 0 31829 0
[pid=28123] vsize: 127896
Current children cumulated CPU time (s) 578.48
Current children cumulated vsize (Kb) 130020

[startup+590.057 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 48695 0 0 0 58663 181 0 0 25 0 1 0 1855507752 131923968 30357 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32208 30357 145 145 0 32063 0
[pid=28123] vsize: 128832
Current children cumulated CPU time (s) 588.46
Current children cumulated vsize (Kb) 130956

[startup+600.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 48923 0 0 0 59659 183 0 0 25 0 1 0 1855507752 132833280 30585 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32430 30585 145 145 0 32285 0
[pid=28123] vsize: 129720
Current children cumulated CPU time (s) 598.44
Current children cumulated vsize (Kb) 131844

[startup+610.059 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 48977 0 0 0 60659 183 0 0 25 0 1 0 1855507752 133050368 30639 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32483 30639 145 145 0 32338 0
[pid=28123] vsize: 129932
Current children cumulated CPU time (s) 608.44
Current children cumulated vsize (Kb) 132056

[startup+620.06 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49005 0 0 0 61658 184 0 0 25 0 1 0 1855507752 133160960 30667 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32510 30667 145 145 0 32365 0
[pid=28123] vsize: 130040
Current children cumulated CPU time (s) 618.44
Current children cumulated vsize (Kb) 132164

[startup+630.061 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49048 0 0 0 62658 184 0 0 25 0 1 0 1855507752 133332992 30710 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32552 30710 145 145 0 32407 0
[pid=28123] vsize: 130208
Current children cumulated CPU time (s) 628.44
Current children cumulated vsize (Kb) 132332

[startup+640.062 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49086 0 0 0 63657 184 0 0 25 0 1 0 1855507752 133484544 30748 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32589 30748 145 145 0 32444 0
[pid=28123] vsize: 130356
Current children cumulated CPU time (s) 638.43
Current children cumulated vsize (Kb) 132480

[startup+650.063 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49104 0 0 0 64657 184 0 0 25 0 1 0 1855507752 133550080 30766 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32605 30766 145 145 0 32460 0
[pid=28123] vsize: 130420
Current children cumulated CPU time (s) 648.43
Current children cumulated vsize (Kb) 132544

[startup+660.064 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49121 0 0 0 65657 184 0 0 25 0 1 0 1855507752 133632000 30783 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32625 30783 145 145 0 32480 0
[pid=28123] vsize: 130500
Current children cumulated CPU time (s) 658.43
Current children cumulated vsize (Kb) 132624

[startup+670.066 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49131 0 0 0 66658 184 0 0 25 0 1 0 1855507752 133672960 30793 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32635 30793 145 145 0 32490 0
[pid=28123] vsize: 130540
Current children cumulated CPU time (s) 668.44
Current children cumulated vsize (Kb) 132664

[startup+680.066 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49143 0 0 0 67658 185 0 0 25 0 1 0 1855507752 133722112 30805 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32647 30805 145 145 0 32502 0
[pid=28123] vsize: 130588
Current children cumulated CPU time (s) 678.45
Current children cumulated vsize (Kb) 132712

[startup+690.066 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49159 0 0 0 68657 185 0 0 25 0 1 0 1855507752 133783552 30821 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32662 30821 145 145 0 32517 0
[pid=28123] vsize: 130648
Current children cumulated CPU time (s) 688.44
Current children cumulated vsize (Kb) 132772

[startup+700.067 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49185 0 0 0 69658 185 0 0 25 0 1 0 1855507752 133890048 30847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32688 30847 145 145 0 32543 0
[pid=28123] vsize: 130752
Current children cumulated CPU time (s) 698.45
Current children cumulated vsize (Kb) 132876

[startup+710.068 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49204 0 0 0 70657 185 0 0 25 0 1 0 1855507752 133959680 30866 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32705 30866 145 145 0 32560 0
[pid=28123] vsize: 130820
Current children cumulated CPU time (s) 708.44
Current children cumulated vsize (Kb) 132944

[startup+720.069 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49218 0 0 0 71658 185 0 0 25 0 1 0 1855507752 134017024 30880 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32719 30880 145 145 0 32574 0
[pid=28123] vsize: 130876
Current children cumulated CPU time (s) 718.45
Current children cumulated vsize (Kb) 133000

[startup+730.07 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49238 0 0 0 72658 185 0 0 25 0 1 0 1855507752 134094848 30900 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32738 30900 145 145 0 32593 0
[pid=28123] vsize: 130952
Current children cumulated CPU time (s) 728.45
Current children cumulated vsize (Kb) 133076

[startup+740.071 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49259 0 0 0 73657 186 0 0 25 0 1 0 1855507752 134176768 30921 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32758 30921 145 145 0 32613 0
[pid=28123] vsize: 131032
Current children cumulated CPU time (s) 738.45
Current children cumulated vsize (Kb) 133156

[startup+750.072 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49269 0 0 0 74658 186 0 0 25 0 1 0 1855507752 134213632 30931 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32767 30931 145 145 0 32622 0
[pid=28123] vsize: 131068
Current children cumulated CPU time (s) 748.46
Current children cumulated vsize (Kb) 133192

[startup+760.073 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49337 0 0 0 75656 186 0 0 25 0 1 0 1855507752 134483968 30999 4294967295 134512640 135094434 3221224432 3221223104 134556300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 32833 30999 145 145 0 32688 0
[pid=28123] vsize: 131332
Current children cumulated CPU time (s) 758.44
Current children cumulated vsize (Kb) 133456

[startup+770.074 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49932 0 0 0 76648 190 0 0 25 0 1 0 1855507752 136876032 31594 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33417 31594 145 145 0 33272 0
[pid=28123] vsize: 133668
Current children cumulated CPU time (s) 768.4
Current children cumulated vsize (Kb) 135792

[startup+780.075 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 49992 0 0 0 77647 191 0 0 25 0 1 0 1855507752 137129984 31654 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33479 31654 145 145 0 33334 0
[pid=28123] vsize: 133916
Current children cumulated CPU time (s) 778.4
Current children cumulated vsize (Kb) 136040

[startup+790.076 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50022 0 0 0 78647 191 0 0 25 0 1 0 1855507752 137252864 31684 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33509 31684 145 145 0 33364 0
[pid=28123] vsize: 134036
Current children cumulated CPU time (s) 788.4
Current children cumulated vsize (Kb) 136160

[startup+800.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50058 0 0 0 79647 191 0 0 25 0 1 0 1855507752 137388032 31720 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33542 31720 145 145 0 33397 0
[pid=28123] vsize: 134168
Current children cumulated CPU time (s) 798.4
Current children cumulated vsize (Kb) 136292

[startup+810.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50075 0 0 0 80646 192 0 0 25 0 1 0 1855507752 137453568 31737 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33558 31737 145 145 0 33413 0
[pid=28123] vsize: 134232
Current children cumulated CPU time (s) 808.4
Current children cumulated vsize (Kb) 136356

[startup+820.078 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50095 0 0 0 81646 192 0 0 25 0 1 0 1855507752 137535488 31757 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33578 31757 145 145 0 33433 0
[pid=28123] vsize: 134312
Current children cumulated CPU time (s) 818.4
Current children cumulated vsize (Kb) 136436

[startup+830.079 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50109 0 0 0 82646 192 0 0 25 0 1 0 1855507752 137588736 31771 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 33591 31771 145 145 0 33446 0
[pid=28123] vsize: 134364
Current children cumulated CPU time (s) 828.4
Current children cumulated vsize (Kb) 136488

[startup+840.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50126 0 0 0 83645 192 0 0 25 0 1 0 1855507752 137654272 31788 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33607 31788 145 145 0 33462 0
[pid=28123] vsize: 134428
Current children cumulated CPU time (s) 838.39
Current children cumulated vsize (Kb) 136552

[startup+850.082 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50139 0 0 0 84645 192 0 0 25 0 1 0 1855507752 137707520 31801 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33620 31801 145 145 0 33475 0
[pid=28123] vsize: 134480
Current children cumulated CPU time (s) 848.39
Current children cumulated vsize (Kb) 136604

[startup+860.083 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50159 0 0 0 85645 193 0 0 25 0 1 0 1855507752 138313728 31821 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33768 31821 145 145 0 33623 0
[pid=28123] vsize: 135072
Current children cumulated CPU time (s) 858.4
Current children cumulated vsize (Kb) 137196

[startup+870.084 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50172 0 0 0 86645 193 0 0 25 0 1 0 1855507752 138358784 31834 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33779 31834 145 145 0 33634 0
[pid=28123] vsize: 135116
Current children cumulated CPU time (s) 868.4
Current children cumulated vsize (Kb) 137240

[startup+880.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50186 0 0 0 87645 193 0 0 25 0 1 0 1855507752 138416128 31848 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33793 31848 145 145 0 33648 0
[pid=28123] vsize: 135172
Current children cumulated CPU time (s) 878.4
Current children cumulated vsize (Kb) 137296

[startup+890.086 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50208 0 0 0 88645 193 0 0 25 0 1 0 1855507752 138502144 31870 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33814 31870 145 145 0 33669 0
[pid=28123] vsize: 135256
Current children cumulated CPU time (s) 888.4
Current children cumulated vsize (Kb) 137380

[startup+900.087 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50373 0 0 0 89643 194 0 0 25 0 1 0 1855507752 139165696 32035 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 33976 32035 145 145 0 33831 0
[pid=28123] vsize: 135904
Current children cumulated CPU time (s) 898.39
Current children cumulated vsize (Kb) 138028

[startup+910.088 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50735 0 0 0 90636 197 0 0 25 0 1 0 1855507752 140627968 32397 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34333 32397 145 145 0 34188 0
[pid=28123] vsize: 137332
Current children cumulated CPU time (s) 908.35
Current children cumulated vsize (Kb) 139456

[startup+920.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50801 0 0 0 91636 197 0 0 25 0 1 0 1855507752 140914688 32463 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34403 32463 145 145 0 34258 0
[pid=28123] vsize: 137612
Current children cumulated CPU time (s) 918.35
Current children cumulated vsize (Kb) 139736

[startup+930.091 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50819 0 0 0 92636 197 0 0 25 0 1 0 1855507752 140988416 32481 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34421 32481 145 145 0 34276 0
[pid=28123] vsize: 137684
Current children cumulated CPU time (s) 928.35
Current children cumulated vsize (Kb) 139808

[startup+940.091 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50849 0 0 0 93635 198 0 0 25 0 1 0 1855507752 141107200 32511 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34450 32511 145 145 0 34305 0
[pid=28123] vsize: 137800
Current children cumulated CPU time (s) 938.35
Current children cumulated vsize (Kb) 139924

[startup+950.092 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50865 0 0 0 94635 198 0 0 25 0 1 0 1855507752 141168640 32527 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34465 32527 145 145 0 34320 0
[pid=28123] vsize: 137860
Current children cumulated CPU time (s) 948.35
Current children cumulated vsize (Kb) 139984

[startup+960.093 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50884 0 0 0 95635 198 0 0 25 0 1 0 1855507752 141242368 32546 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34483 32546 145 145 0 34338 0
[pid=28123] vsize: 137932
Current children cumulated CPU time (s) 958.35
Current children cumulated vsize (Kb) 140056

[startup+970.094 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50917 0 0 0 96635 198 0 0 25 0 1 0 1855507752 141365248 32579 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34513 32579 145 145 0 34368 0
[pid=28123] vsize: 138052
Current children cumulated CPU time (s) 968.35
Current children cumulated vsize (Kb) 140176

[startup+980.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50942 0 0 0 97635 198 0 0 25 0 1 0 1855507752 141463552 32604 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34537 32604 145 145 0 34392 0
[pid=28123] vsize: 138148
Current children cumulated CPU time (s) 978.35
Current children cumulated vsize (Kb) 140272

[startup+990.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 50967 0 0 0 98634 199 0 0 25 0 1 0 1855507752 141561856 32629 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34561 32629 145 145 0 34416 0
[pid=28123] vsize: 138244
Current children cumulated CPU time (s) 988.35
Current children cumulated vsize (Kb) 140368

[startup+1000.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51023 0 0 0 99634 199 0 0 25 0 1 0 1855507752 141783040 32685 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34615 32685 145 145 0 34470 0
[pid=28123] vsize: 138460
Current children cumulated CPU time (s) 998.35
Current children cumulated vsize (Kb) 140584

[startup+1010.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51041 0 0 0 100634 199 0 0 25 0 1 0 1855507752 141852672 32703 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34632 32703 145 145 0 34487 0
[pid=28123] vsize: 138528
Current children cumulated CPU time (s) 1008.35
Current children cumulated vsize (Kb) 140652

[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51054 0 0 0 101634 199 0 0 25 0 1 0 1855507752 141901824 32716 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34644 32716 145 145 0 34499 0
[pid=28123] vsize: 138576
Current children cumulated CPU time (s) 1018.35
Current children cumulated vsize (Kb) 140700

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51069 0 0 0 102634 199 0 0 25 0 1 0 1855507752 141963264 32731 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34659 32731 145 145 0 34514 0
[pid=28123] vsize: 138636
Current children cumulated CPU time (s) 1028.35
Current children cumulated vsize (Kb) 140760

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51084 0 0 0 103634 199 0 0 25 0 1 0 1855507752 142016512 32746 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34672 32746 145 145 0 34527 0
[pid=28123] vsize: 138688
Current children cumulated CPU time (s) 1038.35
Current children cumulated vsize (Kb) 140812

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51097 0 0 0 104634 199 0 0 25 0 1 0 1855507752 142069760 32759 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34685 32759 145 145 0 34540 0
[pid=28123] vsize: 138740
Current children cumulated CPU time (s) 1048.35
Current children cumulated vsize (Kb) 140864

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51116 0 0 0 105634 199 0 0 25 0 1 0 1855507752 142147584 32778 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34704 32778 145 145 0 34559 0
[pid=28123] vsize: 138816
Current children cumulated CPU time (s) 1058.35
Current children cumulated vsize (Kb) 140940

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51125 0 0 0 106634 199 0 0 25 0 1 0 1855507752 142184448 32787 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34713 32787 145 145 0 34568 0
[pid=28123] vsize: 138852
Current children cumulated CPU time (s) 1068.35
Current children cumulated vsize (Kb) 140976

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51138 0 0 0 107634 199 0 0 25 0 1 0 1855507752 142229504 32800 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34724 32800 145 145 0 34579 0
[pid=28123] vsize: 138896
Current children cumulated CPU time (s) 1078.35
Current children cumulated vsize (Kb) 141020

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51148 0 0 0 108634 199 0 0 25 0 1 0 1855507752 142270464 32810 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34734 32810 145 145 0 34589 0
[pid=28123] vsize: 138936
Current children cumulated CPU time (s) 1088.35
Current children cumulated vsize (Kb) 141060

[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51171 0 0 0 109634 199 0 0 25 0 1 0 1855507752 142360576 32833 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34756 32833 145 145 0 34611 0
[pid=28123] vsize: 139024
Current children cumulated CPU time (s) 1098.35
Current children cumulated vsize (Kb) 141148

[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51179 0 0 0 110634 200 0 0 25 0 1 0 1855507752 142393344 32841 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34764 32841 145 145 0 34619 0
[pid=28123] vsize: 139056
Current children cumulated CPU time (s) 1108.36
Current children cumulated vsize (Kb) 141180

[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51184 0 0 0 111635 200 0 0 25 0 1 0 1855507752 142409728 32846 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34768 32846 145 145 0 34623 0
[pid=28123] vsize: 139072
Current children cumulated CPU time (s) 1118.37
Current children cumulated vsize (Kb) 141196

[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51193 0 0 0 112635 200 0 0 25 0 1 0 1855507752 142446592 32855 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34777 32855 145 145 0 34632 0
[pid=28123] vsize: 139108
Current children cumulated CPU time (s) 1128.37
Current children cumulated vsize (Kb) 141232

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51201 0 0 0 113635 200 0 0 25 0 1 0 1855507752 142479360 32863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28123/statm): 34785 32863 145 145 0 34640 0
[pid=28123] vsize: 139140
Current children cumulated CPU time (s) 1138.37
Current children cumulated vsize (Kb) 141264

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51212 0 0 0 114634 200 0 0 25 0 1 0 1855507752 142520320 32874 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34795 32874 145 145 0 34650 0
[pid=28123] vsize: 139180
Current children cumulated CPU time (s) 1148.36
Current children cumulated vsize (Kb) 141304

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51227 0 0 0 115634 200 0 0 25 0 1 0 1855507752 142577664 32889 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34809 32889 145 145 0 34664 0
[pid=28123] vsize: 139236
Current children cumulated CPU time (s) 1158.36
Current children cumulated vsize (Kb) 141360

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51235 0 0 0 116634 200 0 0 25 0 1 0 1855507752 142610432 32897 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34817 32897 145 145 0 34672 0
[pid=28123] vsize: 139268
Current children cumulated CPU time (s) 1168.36
Current children cumulated vsize (Kb) 141392

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51240 0 0 0 117635 200 0 0 25 0 1 0 1855507752 142630912 32902 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34822 32902 145 145 0 34677 0
[pid=28123] vsize: 139288
Current children cumulated CPU time (s) 1178.37
Current children cumulated vsize (Kb) 141412

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51262 0 0 0 118634 200 0 0 25 0 1 0 1855507752 142716928 32924 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34843 32924 145 145 0 34698 0
[pid=28123] vsize: 139372
Current children cumulated CPU time (s) 1188.36
Current children cumulated vsize (Kb) 141496

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51280 0 0 0 119634 201 0 0 25 0 1 0 1855507752 142786560 32942 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34860 32942 145 145 0 34715 0
[pid=28123] vsize: 139440
Current children cumulated CPU time (s) 1198.37
Current children cumulated vsize (Kb) 141564

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51324 0 0 0 120634 201 0 0 25 0 1 0 1855507752 142958592 32986 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34902 32986 145 145 0 34757 0
[pid=28123] vsize: 139608
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 141732



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 28123
Raw data (/proc/28119/stat): 28119 (minisat+_script) S 28118 28119 31027 0 -1 0 289 239 0 0 0 1 0 1 16 0 1 0 1855507747 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28119/statm): 531 226 485 147 0 384 0
[pid=28119] vsize: 2124
Raw data (/proc/28123/stat): 28123 (minisat+_64-bit) R 28119 28119 31027 0 -1 0 51324 0 0 0 120634 201 0 0 25 0 1 0 1855507752 142958592 32986 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28123/statm): 34902 32986 145 145 0 34757 0
[pid=28123] vsize: 139608
Current children cumulated CPU time (s) 1208.37
Current children cumulated vsize (Kb) 141732

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

Child status: 0
Real time (s): 1210.18
CPU time (s): 1208.42
CPU user time (s): 1206.34
CPU system time (s): 2.07868
CPU usage (%): 99.8543
Max. virtual memory (cumulated for all children) (Kb): 141732

Verifier Data

ERROR: no interpretation found !