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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nsrand-ipx.opb
MD5SUM6b39a5ca45e18a6e9e3dc91f7594e22c
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1258323967
Optimality of the best value was proved NO
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1073741824
Number of bits of the biggest number in a constraint 31
Biggest sum of numbers in a constraint 26715880447
Number of bits of the biggest sum of numbers35
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.13
Number of variables6651
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 constraint6651

Trace number 4496

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        935988 kB
Buffers:          2036 kB
Cached:          66828 kB
SwapCached:       1176 kB
Active:          17832 kB
Inactive:        53640 kB
HighTotal:      131008 kB
HighFree:        60452 kB
LowTotal:       903652 kB
LowFree:        875536 kB
SwapTotal:     2097136 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            21396 kB
Committed_AS:    92588 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:03:21 (client local time) WITH STATUS 0 IN 1208.5 SECONDS
stats: 2956 7 1208.5 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: 38230   maxlim: 24568396799   bits: 35/35
c ---[1048]---> BDD-cost:   37
c ---[1047]---> BDD-cost:   37
c ---[1046]---> BDD-cost:   37
c ---[1045]---> BDD-cost:   37
c ---[1044]---> BDD-cost:   37
c ---[1043]---> BDD-cost:   37
c ---[1042]---> BDD-cost:   37
c ---[1041]---> BDD-cost:   37
c ---[1040]---> BDD-cost:   37
c ---[1039]---> BDD-cost:   37
c ---[1038]---> BDD-cost:   37
c ---[1037]---> BDD-cost:   37
c ---[1036]---> BDD-cost:   37
c ---[1035]---> BDD-cost:   37
c ---[1034]---> BDD-cost:   37
c ---[1033]---> BDD-cost:   37
c ---[1032]---> BDD-cost:   37
c ---[1031]---> BDD-cost:   37
c ---[1030]---> BDD-cost:   37
c ---[1029]---> BDD-cost:   37
c ---[1028]---> BDD-cost:   37
c ---[1027]---> BDD-cost:   37
c ---[1026]---> BDD-cost:   37
c ---[1025]---> BDD-cost:   37
c ---[1024]---> BDD-cost:   37
c ---[1023]---> BDD-cost:   37
c ---[1022]---> BDD-cost:   37
c ---[1021]---> BDD-cost:   37
c ---[1020]---> BDD-cost:   37
c ---[1019]---> BDD-cost:   37
c ---[1018]---> BDD-cost:   37
c ---[1017]---> BDD-cost:   37
c ---[1016]---> BDD-cost:   37
c ---[1015]---> BDD-cost:   37
c ---[1014]---> BDD-cost:   37
c ---[1013]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   37
c ---[1011]---> BDD-cost:   37
c ---[1010]---> BDD-cost:   37
c ---[1009]---> BDD-cost:   37
c ---[1008]---> BDD-cost:   37
c ---[1007]---> BDD-cost:   37
c ---[1006]---> BDD-cost:   37
c ---[1005]---> BDD-cost:   37
c ---[1004]---> BDD-cost:   37
c ---[1003]---> BDD-cost:   37
c ---[1002]---> BDD-cost:   37
c ---[1001]---> BDD-cost:   37
c ---[1000]---> BDD-cost:   37
c ---[ 999]---> BDD-cost:   37
c ---[ 998]---> BDD-cost:   37
c ---[ 997]---> BDD-cost:   37
c ---[ 996]---> BDD-cost:   37
c ---[ 995]---> BDD-cost:   37
c ---[ 994]---> BDD-cost:   37
c ---[ 993]---> BDD-cost:   37
c ---[ 992]---> BDD-cost:   37
c ---[ 991]---> BDD-cost:   37
c ---[ 990]---> BDD-cost:   37
c ---[ 989]---> BDD-cost:   37
c ---[ 988]---> BDD-cost:   37
c ---[ 987]---> BDD-cost:   37
c ---[ 986]---> BDD-cost:   37
c ---[ 985]---> BDD-cost:   37
c ---[ 984]---> BDD-cost:   37
c ---[ 983]---> BDD-cost:   37
c ---[ 982]---> BDD-cost:   37
c ---[ 981]---> BDD-cost:   37
c ---[ 980]---> BDD-cost:   37
c ---[ 979]---> BDD-cost:   37
c ---[ 978]---> BDD-cost:   37
c ---[ 977]---> BDD-cost:   37
c ---[ 976]---> BDD-cost:   37
c ---[ 975]---> BDD-cost:   37
c ---[ 974]---> BDD-cost:   37
c ---[ 973]---> BDD-cost:   37
c ---[ 972]---> BDD-cost:   37
c ---[ 971]---> BDD-cost:   37
c ---[ 970]---> BDD-cost:   37
c ---[ 969]---> BDD-cost:   37
c ---[ 968]---> BDD-cost:   37
c ---[ 967]---> BDD-cost:   37
c ---[ 966]---> BDD-cost:   37
c ---[ 965]---> BDD-cost:   37
c ---[ 964]---> BDD-cost:   37
c ---[ 963]---> BDD-cost:   37
c ---[ 962]---> BDD-cost:   37
c ---[ 961]---> BDD-cost:   37
c ---[ 960]---> BDD-cost:   37
c ---[ 959]---> BDD-cost:   37
c ---[ 958]---> BDD-cost:   37
c ---[ 957]---> BDD-cost:   37
c ---[ 956]---> BDD-cost:   37
c ---[ 955]---> BDD-cost:   37
c ---[ 954]---> BDD-cost:   37
c ---[ 953]---> BDD-cost:   37
c ---[ 952]---> BDD-cost:   37
c ---[ 951]---> BDD-cost:   37
c ---[ 950]---> BDD-cost:   37
c ---[ 949]---> BDD-cost:   37
c ---[ 948]---> BDD-cost:   37
c ---[ 947]---> BDD-cost:   37
c ---[ 946]---> BDD-cost:   37
c ---[ 945]---> BDD-cost:   37
c ---[ 944]---> BDD-cost:   37
c ---[ 943]---> BDD-cost:   37
c ---[ 942]---> BDD-cost:   37
c ---[ 941]---> BDD-cost:   37
c ---[ 940]---> BDD-cost:   37
c ---[ 939]---> BDD-cost:   37
c ---[ 938]---> BDD-cost:   37
c ---[ 937]---> BDD-cost:   37
c ---[ 936]---> BDD-cost:   37
c ---[ 935]---> BDD-cost:   37
c ---[ 934]---> BDD-cost:   37
c ---[ 933]---> BDD-cost:   37
c ---[ 932]---> BDD-cost:   37
c ---[ 931]---> BDD-cost:   37
c ---[ 930]---> BDD-cost:   37
c ---[ 929]---> BDD-cost:   37
c ---[ 928]---> BDD-cost:   37
c ---[ 927]---> BDD-cost:   37
c ---[ 926]---> BDD-cost:   37
c ---[ 925]---> BDD-cost:   37
c ---[ 924]---> BDD-cost:   37
c ---[ 923]---> BDD-cost:   37
c ---[ 922]---> BDD-cost:   37
c ---[ 921]---> BDD-cost:   37
c ---[ 920]---> BDD-cost:   37
c ---[ 919]---> BDD-cost:   37
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:   37
c ---[ 912]---> BDD-cost:   37
c ---[ 911]---> BDD-cost:   37
c ---[ 910]---> BDD-cost:   37
c ---[ 909]---> BDD-cost:   37
c ---[ 908]---> BDD-cost:   37
c ---[ 907]---> BDD-cost:   37
c ---[ 906]---> BDD-cost:   37
c ---[ 905]---> BDD-cost:   37
c ---[ 904]---> BDD-cost:   37
c ---[ 903]---> BDD-cost:   37
c ---[ 902]---> BDD-cost:   37
c ---[ 901]---> BDD-cost:   37
c ---[ 900]---> BDD-cost:   37
c ---[ 899]---> BDD-cost:   37
c ---[ 898]---> BDD-cost:   37
c ---[ 897]---> BDD-cost:   37
c ---[ 896]---> BDD-cost:   37
c ---[ 895]---> BDD-cost:   37
c ---[ 894]---> BDD-cost:   37
c ---[ 893]---> BDD-cost:   37
c ---[ 892]---> BDD-cost:   37
c ---[ 891]---> BDD-cost:   37
c ---[ 890]---> BDD-cost:   37
c ---[ 889]---> BDD-cost:   37
c ---[ 888]---> BDD-cost:   37
c ---[ 887]---> BDD-cost:   37
c ---[ 886]---> BDD-cost:   37
c ---[ 885]---> BDD-cost:   37
c ---[ 884]---> BDD-cost:   37
c ---[ 883]---> BDD-cost:   37
c ---[ 882]---> BDD-cost:   37
c ---[ 881]---> BDD-cost:   37
c ---[ 880]---> BDD-cost:   37
c ---[ 879]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   37
c ---[ 877]---> BDD-cost:   37
c ---[ 876]---> BDD-cost:   37
c ---[ 875]---> BDD-cost:   37
c ---[ 874]---> BDD-cost:   37
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   37
c ---[ 871]---> BDD-cost:   37
c ---[ 870]---> BDD-cost:   37
c ---[ 869]---> BDD-cost:   37
c ---[ 868]---> BDD-cost:   37
c ---[ 867]---> BDD-cost:   37
c ---[ 866]---> BDD-cost:   37
c ---[ 865]---> BDD-cost:   37
c ---[ 864]---> BDD-cost:   37
c ---[ 863]---> BDD-cost:   37
c ---[ 862]---> BDD-cost:   37
c ---[ 861]---> BDD-cost:   37
c ---[ 860]---> BDD-cost:   37
c ---[ 859]---> BDD-cost:   37
c ---[ 858]---> BDD-cost:   37
c ---[ 857]---> BDD-cost:   37
c ---[ 856]---> BDD-cost:   37
c ---[ 855]---> BDD-cost:   37
c ---[ 854]---> BDD-cost:   37
c ---[ 853]---> BDD-cost:   37
c ---[ 852]---> BDD-cost:   37
c ---[ 851]---> BDD-cost:   37
c ---[ 850]---> BDD-cost:   37
c ---[ 849]---> BDD-cost:   37
c ---[ 848]---> BDD-cost:   37
c ---[ 847]---> BDD-cost:   37
c ---[ 846]---> BDD-cost:   37
c ---[ 845]---> BDD-cost:   37
c ---[ 844]---> BDD-cost:   37
c ---[ 843]---> BDD-cost:   37
c ---[ 842]---> BDD-cost:   37
c ---[ 841]---> BDD-cost:   37
c ---[ 840]---> BDD-cost:   37
c ---[ 839]---> BDD-cost:   37
c ---[ 838]---> BDD-cost:   37
c ---[ 837]---> BDD-cost:   37
c ---[ 836]---> BDD-cost:   37
c ---[ 835]---> BDD-cost:   37
c ---[ 834]---> BDD-cost:   37
c ---[ 833]---> BDD-cost:   37
c ---[ 832]---> BDD-cost:   37
c ---[ 831]---> BDD-cost:   37
c ---[ 830]---> BDD-cost:   37
c ---[ 829]---> BDD-cost:   37
c ---[ 828]---> BDD-cost:   37
c ---[ 827]---> BDD-cost:   37
c ---[ 826]---> BDD-cost:   37
c ---[ 825]---> BDD-cost:   37
c ---[ 824]---> BDD-cost:   37
c ---[ 823]---> BDD-cost:   37
c ---[ 822]---> BDD-cost:   37
c ---[ 821]---> BDD-cost:   37
c ---[ 820]---> BDD-cost:   37
c ---[ 819]---> BDD-cost:   37
c ---[ 818]---> BDD-cost:   37
c ---[ 817]---> BDD-cost:   37
c ---[ 816]---> BDD-cost:   37
c ---[ 815]---> BDD-cost:   37
c ---[ 814]---> BDD-cost:   37
c ---[ 813]---> BDD-cost:   37
c ---[ 812]---> BDD-cost:   37
c ---[ 811]---> BDD-cost:   37
c ---[ 810]---> BDD-cost:   37
c ---[ 809]---> BDD-cost:   37
c ---[ 808]---> BDD-cost:   37
c ---[ 807]---> BDD-cost:   37
c ---[ 806]---> BDD-cost:   37
c ---[ 805]---> BDD-cost:   37
c ---[ 804]---> BDD-cost:   37
c ---[ 803]---> BDD-cost:   37
c ---[ 802]---> BDD-cost:   37
c ---[ 801]---> BDD-cost:   37
c ---[ 800]---> BDD-cost:   37
c ---[ 799]---> BDD-cost:   37
c ---[ 798]---> BDD-cost:   37
c ---[ 797]---> BDD-cost:   37
c ---[ 796]---> BDD-cost:   37
c ---[ 795]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   37
c ---[ 793]---> BDD-cost:   37
c ---[ 792]---> BDD-cost:   37
c ---[ 791]---> BDD-cost:   37
c ---[ 790]---> BDD-cost:   37
c ---[ 783]---> BDD-cost:   37
c ---[ 772]---> BDD-cost:   37
c ---[ 761]---> BDD-cost:   37
c ---[ 750]---> BDD-cost:   37
c ---[ 739]---> BDD-cost:   37
c ---[ 728]---> BDD-cost:   37
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   37
c ---[ 705]---> BDD-cost:   37
c ---[ 694]---> BDD-cost:   37
c ---[ 683]---> BDD-cost:   37
c ---[ 672]---> BDD-cost:   37
c ---[ 661]---> BDD-cost:   37
c ---[ 650]---> BDD-cost:   37
c ---[ 639]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 608]---> BDD-cost:   37
c ---[ 607]---> BDD-cost:   37
c ---[ 600]---> Adder-cost: 2264   maxlim: 44   bits: 7/6
c ---[ 599]---> Adder-cost: 1410   maxlim: 36   bits: 7/6
c ---[ 598]---> Adder-cost: 1190   maxlim: 36   bits: 7/6
c ---[ 597]---> BDD-cost:   37
c ---[ 587]---> BDD-cost:   37
c ---[ 582]---> Adder-cost: 2364   maxlim: 37   bits: 7/6
c ---[ 581]---> Adder-cost: 1680   maxlim: 32   bits: 7/6
c ---[ 576]---> BDD-cost:   37
c ---[ 567]---> BDD-cost:   37
c ---[ 556]---> BDD-cost:   37
c ---[ 546]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   37
c ---[ 525]---> BDD-cost:   37
c ---[ 514]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   37
c ---[ 502]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   37
c ---[ 482]---> BDD-cost:   37
c ---[ 472]---> BDD-cost:   37
c ---[ 462]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   37
c ---[ 440]---> BDD-cost:   37
c ---[ 429]---> BDD-cost:   37
c ---[ 418]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 396]---> BDD-cost:   37
c ---[ 395]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   37
c ---[ 373]---> BDD-cost:   37
c ---[ 363]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   37
c ---[ 355]---> BDD-cost:   37
c ---[ 354]---> BDD-cost:   37
c ---[ 353]---> BDD-cost:   37
c ---[ 352]---> BDD-cost:   37
c ---[ 351]---> BDD-cost:   37
c ---[ 350]---> BDD-cost:   37
c ---[ 349]---> BDD-cost:   37
c ---[ 348]---> BDD-cost:   37
c ---[ 347]---> BDD-cost:   37
c ---[ 346]---> BDD-cost:   37
c ---[ 345]---> BDD-cost:   37
c ---[ 344]---> BDD-cost:   37
c ---[ 343]---> BDD-cost:   37
c ---[ 342]---> BDD-cost:   37
c ---[ 341]---> BDD-cost:   37
c ---[ 340]---> BDD-cost:   37
c ---[ 339]---> BDD-cost:   37
c ---[ 338]---> BDD-cost:   37
c ---[ 337]---> BDD-cost:   37
c ---[ 336]---> BDD-cost:   37
c ---[ 335]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   37
c ---[ 333]---> BDD-cost:   37
c ---[ 332]---> BDD-cost:   37
c ---[ 331]---> BDD-cost:   37
c ---[ 330]---> BDD-cost:   37
c ---[ 329]---> BDD-cost:   37
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: 626   maxlim: 14   bits: 5/4
c ---[ 321]---> Adder-cost: 344   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: 2950   maxlim: 17   bits: 6/5
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost: 2736
c ---[ 270]---> Adder-cost: 2699   maxlim: 19   bits: 6/5
c ---[ 269]---> BDD-cost:  492
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> Adder-cost: 748   maxlim: 16   bits: 6/5
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:   72
c ---[ 264]---> BDD-cost:  100
c ---[ 263]---> Adder-cost: 1013   maxlim: 19   bits: 6/5
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    2
c ---[ 260]---> Adder-cost: 446   maxlim: 18   bits: 6/5
c ---[ 259]---> BDD-cost:  767
c ---[ 258]---> Adder-cost: 912   maxlim: 9   bits: 5/4
c ---[ 257]---> Adder-cost: 1474   maxlim: 21   bits: 6/5
c ---[ 256]---> BDD-cost:  889
c ---[ 255]---> Adder-cost: 1032   maxlim: 17   bits: 6/5
c ---[ 254]---> Adder-cost: 577   maxlim: 9   bits: 5/4
c ---[ 253]---> BDD-cost: 1704
c ---[ 252]---> Adder-cost: 371   maxlim: 19   bits: 6/5
c ---[ 251]---> BDD-cost:  932
c ---[ 250]---> Adder-cost: 1365   maxlim: 24   bits: 6/5
c ---[ 249]---> BDD-cost: 1516
c ---[ 248]---> Adder-cost: 1521   maxlim: 17   bits: 6/5
c ---[ 247]---> BDD-cost:  242
c ---[ 246]---> Adder-cost: 324   maxlim: 24   bits: 6/5
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> Adder-cost: 749   maxlim: 20   bits: 6/5
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> Adder-cost: 615   maxlim: 17   bits: 6/5
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:  497
c ---[ 239]---> Adder-cost: 430   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: 523   maxlim: 17   bits: 6/5
c ---[ 225]---> Adder-cost: 610   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: 1994   maxlim: 23   bits: 6/5
c ---[ 216]---> BDD-cost:  135
c ---[ 215]---> Adder-cost: 902   maxlim: 19   bits: 6/5
c ---[ 214]---> BDD-cost: 1261
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> Adder-cost: 509   maxlim: 20   bits: 6/5
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:  382
c ---[ 206]---> BDD-cost:  656
c ---[ 205]---> Adder-cost: 1492   maxlim: 16   bits: 6/5
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:  308
c ---[ 202]---> Adder-cost: 508   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: 858   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: 748   maxlim: 28   bits: 6/5
c ---[ 190]---> BDD-cost:  156
c ---[ 189]---> Adder-cost: 568   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: 805   maxlim: 16   bits: 6/5
c ---[ 179]---> Adder-cost: 988   maxlim: 20   bits: 6/5
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> Adder-cost: 802   maxlim: 17   bits: 6/5
c ---[ 176]---> Adder-cost: 516   maxlim: 16   bits: 6/5
c ---[ 175]---> Adder-cost: 607   maxlim: 20   bits: 6/5
c ---[ 174]---> BDD-cost:   18
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> Adder-cost: 565   maxlim: 17   bits: 6/5
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 169]---> Adder-cost: 262   maxlim: 22   bits: 6/5
c ---[ 168]---> Adder-cost: 539   maxlim: 20   bits: 6/5
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> Adder-cost: 343   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: 2678   maxlim: 22   bits: 6/5
c ---[ 141]---> Adder-cost: 1141   maxlim: 12   bits: 5/4
c ---[ 140]---> Adder-cost: 1301   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: 1099   maxlim: 12   bits: 5/4
c ---[ 135]---> BDD-cost:  232
c ---[ 134]---> BDD-cost: 1615
c ---[ 133]---> Adder-cost: 2350   maxlim: 19   bits: 6/5
c ---[ 132]---> BDD-cost: 2419
c ---[ 131]---> Adder-cost: 1509   maxlim: 17   bits: 6/5
c ---[ 130]---> BDD-cost: 1026
c ---[ 129]---> BDD-cost: 1706
c ---[ 128]---> BDD-cost:  242
c ---[ 127]---> Adder-cost: 1293   maxlim: 14   bits: 5/4
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> Adder-cost: 539   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: 603   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: 1073   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: 698   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: 479   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: 635   maxlim: 19   bits: 6/5
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:  688
c ---[  77]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[  76]---> BDD-cost:   96
c ---[  75]---> BDD-cost:    1
c ---[  74]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[  73]---> BDD-cost:  161
c ---[  72]---> BDD-cost:  170
c ---[  71]---> Adder-cost: 513   maxlim: 18   bits: 6/5
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> Adder-cost: 215   maxlim: 19   bits: 6/5
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> Adder-cost: 291   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: 480   maxlim: 10   bits: 5/4
c ---[  48]---> Adder-cost: 807   maxlim: 22   bits: 6/5
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   86
c ---[  45]---> BDD-cost:  971
c ---[  44]---> Adder-cost: 1489   maxlim: 21   bits: 6/5
c ---[  43]---> BDD-cost:  173
c ---[  42]---> Adder-cost: 687   maxlim: 10   bits: 5/4
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:  170
c ---[  39]---> Adder-cost: 793   maxlim: 19   bits: 6/5
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  35]---> BDD-cost:   78
c ---[  34]---> BDD-cost:   98
c ---[  33]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> Adder-cost: 687   maxlim: 17   bits: 6/5
c ---[  29]---> BDD-cost:    1
c ---[  28]---> Adder-cost: 542   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: 743   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 |  890342  3228172 |  296780       0        0     nan |  0.000 % |
c |       100 |  890342  3228172 |  326458     100      391     3.9 |  0.500 % |
c |       250 |  890342  3228172 |  359103     250     1189     4.8 |  0.500 % |
c |       475 |  890342  3228172 |  395014     475     2169     4.6 |  0.500 % |
c |       812 |  890342  3228172 |  434515     812     4071     5.0 |  0.500 % |
c |      1318 |  890289  3227973 |  477967    1315     7137     5.4 |  0.500 % |
c |      2077 |  890235  3227771 |  525763    2069    13297     6.4 |  0.502 % |
c |      3216 |  890141  3227421 |  578340    3201    22061     6.9 |  0.504 % |
c |      4924 |  890090  3227230 |  636174    4906    37004     7.5 |  0.505 % |
c |      7486 |  890061  3227123 |  699791    7465    60333     8.1 |  0.506 % |
c |     11330 |  890061  3227123 |  769770   11309   103784     9.2 |  0.506 % |
c |     17096 |  889945  3226691 |  846747   17070   153842     9.0 |  0.507 % |
c |     25746 |  889777  3226077 |  931422   25697   227105     8.8 |  0.514 % |
c |     38720 |  889165  3223843 | 1024565   38622   346417     9.0 |  0.534 % |
c |     58182 |  889134  3223728 | 1127021   58081   922227    15.9 |  0.535 % |
c |     87375 |  889087  3223555 | 1239723   87272  1737010    19.9 |  0.536 % |
c |    131164 |  886745  3215029 | 1363696  130863  2238984    17.1 |  0.632 % |

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/11152/stat): 11152 (minisat+_script) R 11151 11152 10120 0 -1 0 18 0 0 0 0 0 0 0 22 0 1 0 1736702643 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/11152/statm): 174 3 169 147 0 27 0
[pid=11152] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
open syscall for file /usr/lib/gconv/gconv-modules.cache
New process pid=11153
New process pid=11154
New process pid=11155
execve syscall for /bin/sed executable
One traced child (pid=11154) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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
open syscall for file /usr/lib/locale/locale-archive
open syscall for file /usr/lib/gconv/gconv-modules.cache
One traced child (pid=11155) exited with status: 0
One traced child (pid=11153) exited with status: 0
New process pid=11156
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-nsrand-ipx.opb

[startup+10.0032 s]
Raw data (loadavg): 0.90 0.93 0.80 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 8072 0 0 0 934 32 0 0 25 0 1 0 1736702649 25169920 5575 4294967295 134512640 135094434 3221221600 3221217040 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 6145 5575 145 145 0 6000 0
[pid=11156] vsize: 24580
Current children cumulated CPU time (s) 9.67
Current children cumulated vsize (Kb) 28776

[startup+20.004 s]
Raw data (loadavg): 0.92 0.93 0.80 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 11921 0 0 0 1919 42 0 0 25 0 1 0 1736702649 24748032 5492 4294967295 134512640 135094434 3221221600 3221217920 134677330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 6042 5492 145 145 0 5897 0
[pid=11156] vsize: 24168
Current children cumulated CPU time (s) 19.62
Current children cumulated vsize (Kb) 28364

[startup+30.0058 s]
Raw data (loadavg): 0.93 0.93 0.80 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 16126 0 0 0 2906 50 0 0 25 0 1 0 1736702649 24649728 5465 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 6018 5465 145 145 0 5873 0
[pid=11156] vsize: 24072
Current children cumulated CPU time (s) 29.57
Current children cumulated vsize (Kb) 28268

[startup+40.0056 s]
Raw data (loadavg): 0.94 0.93 0.80 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 20343 0 0 0 3893 58 0 0 25 0 1 0 1736702649 24715264 5479 4294967295 134512640 135094434 3221221600 3221218244 134676244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 6034 5479 145 145 0 5889 0
[pid=11156] vsize: 24136
Current children cumulated CPU time (s) 39.52
Current children cumulated vsize (Kb) 28332

[startup+50.0084 s]
Raw data (loadavg): 0.95 0.94 0.81 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 24532 0 0 0 4876 70 0 0 25 0 1 0 1736702649 24977408 5534 4294967295 134512640 135094434 3221221600 3221217744 134601016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 6098 5534 145 145 0 5953 0
[pid=11156] vsize: 24392
Current children cumulated CPU time (s) 49.47
Current children cumulated vsize (Kb) 28588

[startup+60.0091 s]
Raw data (loadavg): 0.96 0.94 0.81 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 28901 0 0 0 5860 80 0 0 25 0 1 0 1736702649 24682496 5478 4294967295 134512640 135094434 3221221600 3221218272 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 6026 5478 145 145 0 5881 0
[pid=11156] vsize: 24104
Current children cumulated CPU time (s) 59.41
Current children cumulated vsize (Kb) 28300

[startup+70.0109 s]
Raw data (loadavg): 0.96 0.94 0.81 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 33230 0 0 0 6846 89 0 0 25 0 1 0 1736702649 24158208 5366 4294967295 134512640 135094434 3221221600 3221219504 134676480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 5898 5366 145 145 0 5753 0
[pid=11156] vsize: 23592
Current children cumulated CPU time (s) 69.36
Current children cumulated vsize (Kb) 27788

[startup+80.0127 s]
Raw data (loadavg): 0.97 0.94 0.81 1/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 39510 0 0 0 7822 105 0 0 25 0 1 0 1736702649 31068160 7085 4294967295 134512640 135094434 3221221600 3221216060 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11156/statm): 7585 7085 145 145 0 7440 0
[pid=11156] vsize: 30340
Current children cumulated CPU time (s) 79.28
Current children cumulated vsize (Kb) 34536

[startup+90.0135 s]
Raw data (loadavg): 0.97 0.94 0.81 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 48062 0 0 0 8779 134 0 0 25 0 1 0 1736702649 60497920 13660 4294967295 134512640 135094434 3221221600 3221219248 134519312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 14770 13660 145 145 0 14625 0
[pid=11156] vsize: 59080
Current children cumulated CPU time (s) 89.14
Current children cumulated vsize (Kb) 63276

[startup+100.014 s]
Raw data (loadavg): 0.98 0.94 0.82 1/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 58566 0 0 0 9694 176 0 0 21 0 1 0 1736702649 108564480 24143 4294967295 134512640 135094434 3221221600 3221217036 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11156/statm): 26505 24143 145 145 0 26360 0
[pid=11156] vsize: 106020
Current children cumulated CPU time (s) 98.71
Current children cumulated vsize (Kb) 110216

[startup+110.015 s]
Raw data (loadavg): 0.98 0.94 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 59825 0 0 0 10678 183 0 0 25 0 1 0 1736702649 113287168 25402 4294967295 134512640 135094434 3221221600 3221220256 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 27658 25402 145 145 0 27513 0
[pid=11156] vsize: 110632
Current children cumulated CPU time (s) 108.62
Current children cumulated vsize (Kb) 114828

[startup+120.016 s]
Raw data (loadavg): 0.98 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60045 0 0 0 11673 186 0 0 25 0 1 0 1736702649 114176000 25622 4294967295 134512640 135094434 3221221600 3221220256 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 27875 25622 145 145 0 27730 0
[pid=11156] vsize: 111500
Current children cumulated CPU time (s) 118.6
Current children cumulated vsize (Kb) 115696

[startup+130.017 s]
Raw data (loadavg): 0.98 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60272 0 0 0 12670 187 0 0 25 0 1 0 1736702649 115040256 25849 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28086 25849 145 145 0 27941 0
[pid=11156] vsize: 112344
Current children cumulated CPU time (s) 128.58
Current children cumulated vsize (Kb) 116540

[startup+140.017 s]
Raw data (loadavg): 0.99 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60475 0 0 0 13667 189 0 0 25 0 1 0 1736702649 115818496 26052 4294967295 134512640 135094434 3221221600 3221220212 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28276 26052 145 145 0 28131 0
[pid=11156] vsize: 113104
Current children cumulated CPU time (s) 138.57
Current children cumulated vsize (Kb) 117300

[startup+150.018 s]
Raw data (loadavg): 0.99 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60556 0 0 0 14665 190 0 0 25 0 1 0 1736702649 116129792 26133 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28352 26133 145 145 0 28207 0
[pid=11156] vsize: 113408
Current children cumulated CPU time (s) 148.56
Current children cumulated vsize (Kb) 117604

[startup+160.019 s]
Raw data (loadavg): 0.99 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60597 0 0 0 15665 190 0 0 25 0 1 0 1736702649 116293632 26174 4294967295 134512640 135094434 3221221600 3221220256 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28392 26174 145 145 0 28247 0
[pid=11156] vsize: 113568
Current children cumulated CPU time (s) 158.56
Current children cumulated vsize (Kb) 117764

[startup+170.019 s]
Raw data (loadavg): 0.99 0.95 0.82 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60647 0 0 0 16664 190 0 0 25 0 1 0 1736702649 116453376 26224 4294967295 134512640 135094434 3221221600 3221220212 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28431 26224 145 145 0 28286 0
[pid=11156] vsize: 113724
Current children cumulated CPU time (s) 168.55
Current children cumulated vsize (Kb) 117920

[startup+180.019 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60704 0 0 0 17664 191 0 0 25 0 1 0 1736702649 116707328 26281 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28493 26281 145 145 0 28348 0
[pid=11156] vsize: 113972
Current children cumulated CPU time (s) 178.56
Current children cumulated vsize (Kb) 118168

[startup+190.02 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60728 0 0 0 18663 191 0 0 25 0 1 0 1736702649 116781056 26305 4294967295 134512640 135094434 3221221600 3221220212 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 28511 26305 145 145 0 28366 0
[pid=11156] vsize: 114044
Current children cumulated CPU time (s) 188.55
Current children cumulated vsize (Kb) 118240

[startup+200.021 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60742 0 0 0 19663 192 0 0 25 0 1 0 1736702649 116834304 26319 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 28524 26319 145 145 0 28379 0
[pid=11156] vsize: 114096
Current children cumulated CPU time (s) 198.56
Current children cumulated vsize (Kb) 118292

[startup+210.022 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60755 0 0 0 20661 192 0 0 25 0 1 0 1736702649 116887552 26332 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 28537 26332 145 145 0 28392 0
[pid=11156] vsize: 114148
Current children cumulated CPU time (s) 208.54
Current children cumulated vsize (Kb) 118344

[startup+220.023 s]
Raw data (loadavg): 0.99 0.95 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60770 0 0 0 21661 192 0 0 25 0 1 0 1736702649 116944896 26347 4294967295 134512640 135094434 3221221600 3221220224 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28551 26347 145 145 0 28406 0
[pid=11156] vsize: 114204
Current children cumulated CPU time (s) 218.54
Current children cumulated vsize (Kb) 118400

[startup+230.023 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60782 0 0 0 22661 192 0 0 25 0 1 0 1736702649 116989952 26359 4294967295 134512640 135094434 3221221600 3221220256 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28562 26359 145 145 0 28417 0
[pid=11156] vsize: 114248
Current children cumulated CPU time (s) 228.54
Current children cumulated vsize (Kb) 118444

[startup+240.024 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60792 0 0 0 23661 192 0 0 25 0 1 0 1736702649 117030912 26369 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28572 26369 145 145 0 28427 0
[pid=11156] vsize: 114288
Current children cumulated CPU time (s) 238.54
Current children cumulated vsize (Kb) 118484

[startup+250.025 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60805 0 0 0 24661 192 0 0 25 0 1 0 1736702649 117080064 26382 4294967295 134512640 135094434 3221221600 3221220212 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28584 26382 145 145 0 28439 0
[pid=11156] vsize: 114336
Current children cumulated CPU time (s) 248.54
Current children cumulated vsize (Kb) 118532

[startup+260.026 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60814 0 0 0 25661 192 0 0 25 0 1 0 1736702649 117116928 26391 4294967295 134512640 135094434 3221221600 3221220224 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28593 26391 145 145 0 28448 0
[pid=11156] vsize: 114372
Current children cumulated CPU time (s) 258.54
Current children cumulated vsize (Kb) 118568

[startup+270.026 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60825 0 0 0 26660 193 0 0 25 0 1 0 1736702649 117157888 26402 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28603 26402 145 145 0 28458 0
[pid=11156] vsize: 114412
Current children cumulated CPU time (s) 268.54
Current children cumulated vsize (Kb) 118608

[startup+280.026 s]
Raw data (loadavg): 0.99 0.96 0.83 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60835 0 0 0 27661 193 0 0 25 0 1 0 1736702649 117198848 26412 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28613 26412 145 145 0 28468 0
[pid=11156] vsize: 114452
Current children cumulated CPU time (s) 278.55
Current children cumulated vsize (Kb) 118648

[startup+290.027 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60848 0 0 0 28661 193 0 0 25 0 1 0 1736702649 117248000 26425 4294967295 134512640 135094434 3221221600 3221220212 134563112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28625 26425 145 145 0 28480 0
[pid=11156] vsize: 114500
Current children cumulated CPU time (s) 288.55
Current children cumulated vsize (Kb) 118696

[startup+300.028 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60858 0 0 0 29661 193 0 0 25 0 1 0 1736702649 117284864 26435 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28634 26435 145 145 0 28489 0
[pid=11156] vsize: 114536
Current children cumulated CPU time (s) 298.55
Current children cumulated vsize (Kb) 118732

[startup+310.029 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60872 0 0 0 30661 193 0 0 25 0 1 0 1736702649 117342208 26449 4294967295 134512640 135094434 3221221600 3221220288 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28648 26449 145 145 0 28503 0
[pid=11156] vsize: 114592
Current children cumulated CPU time (s) 308.55
Current children cumulated vsize (Kb) 118788

[startup+320.028 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60884 0 0 0 31661 193 0 0 25 0 1 0 1736702649 117387264 26461 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 28659 26461 145 145 0 28514 0
[pid=11156] vsize: 114636
Current children cumulated CPU time (s) 318.55
Current children cumulated vsize (Kb) 118832

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60915 0 0 0 32660 193 0 0 25 0 1 0 1736702649 117456896 26492 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28676 26492 145 145 0 28531 0
[pid=11156] vsize: 114704
Current children cumulated CPU time (s) 328.54
Current children cumulated vsize (Kb) 118900

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60931 0 0 0 33660 194 0 0 25 0 1 0 1736702649 117518336 26508 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28691 26508 145 145 0 28546 0
[pid=11156] vsize: 114764
Current children cumulated CPU time (s) 338.55
Current children cumulated vsize (Kb) 118960

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60945 0 0 0 34660 194 0 0 25 0 1 0 1736702649 117575680 26522 4294967295 134512640 135094434 3221221600 3221220212 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28705 26522 145 145 0 28560 0
[pid=11156] vsize: 114820
Current children cumulated CPU time (s) 348.55
Current children cumulated vsize (Kb) 119016

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60965 0 0 0 35660 194 0 0 25 0 1 0 1736702649 117653504 26542 4294967295 134512640 135094434 3221221600 3221220256 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28724 26542 145 145 0 28579 0
[pid=11156] vsize: 114896
Current children cumulated CPU time (s) 358.55
Current children cumulated vsize (Kb) 119092

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60980 0 0 0 36660 194 0 0 25 0 1 0 1736702649 117710848 26557 4294967295 134512640 135094434 3221221600 3221220260 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28738 26557 145 145 0 28593 0
[pid=11156] vsize: 114952
Current children cumulated CPU time (s) 368.55
Current children cumulated vsize (Kb) 119148

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.84 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 60991 0 0 0 37660 194 0 0 25 0 1 0 1736702649 117751808 26568 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28748 26568 145 145 0 28603 0
[pid=11156] vsize: 114992
Current children cumulated CPU time (s) 378.55
Current children cumulated vsize (Kb) 119188

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61001 0 0 0 38660 194 0 0 25 0 1 0 1736702649 117792768 26578 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28758 26578 145 145 0 28613 0
[pid=11156] vsize: 115032
Current children cumulated CPU time (s) 388.55
Current children cumulated vsize (Kb) 119228

[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61013 0 0 0 39660 194 0 0 25 0 1 0 1736702649 117837824 26590 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28769 26590 145 145 0 28624 0
[pid=11156] vsize: 115076
Current children cumulated CPU time (s) 398.55
Current children cumulated vsize (Kb) 119272

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61057 0 0 0 40660 194 0 0 25 0 1 0 1736702649 118149120 26634 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28845 26634 145 145 0 28700 0
[pid=11156] vsize: 115380
Current children cumulated CPU time (s) 408.55
Current children cumulated vsize (Kb) 119576

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61058 0 0 0 41660 194 0 0 25 0 1 0 1736702649 118149120 26635 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28845 26635 145 145 0 28700 0
[pid=11156] vsize: 115380
Current children cumulated CPU time (s) 418.55
Current children cumulated vsize (Kb) 119576

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61059 0 0 0 42660 194 0 0 25 0 1 0 1736702649 118149120 26636 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28845 26636 145 145 0 28700 0
[pid=11156] vsize: 115380
Current children cumulated CPU time (s) 428.55
Current children cumulated vsize (Kb) 119576

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61073 0 0 0 43660 194 0 0 25 0 1 0 1736702649 118202368 26650 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28858 26650 145 145 0 28713 0
[pid=11156] vsize: 115432
Current children cumulated CPU time (s) 438.55
Current children cumulated vsize (Kb) 119628

[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61086 0 0 0 44660 195 0 0 25 0 1 0 1736702649 118251520 26663 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28870 26663 145 145 0 28725 0
[pid=11156] vsize: 115480
Current children cumulated CPU time (s) 448.56
Current children cumulated vsize (Kb) 119676

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61097 0 0 0 45661 195 0 0 25 0 1 0 1736702649 118296576 26674 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28881 26674 145 145 0 28736 0
[pid=11156] vsize: 115524
Current children cumulated CPU time (s) 458.57
Current children cumulated vsize (Kb) 119720

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61113 0 0 0 46661 195 0 0 25 0 1 0 1736702649 118358016 26690 4294967295 134512640 135094434 3221221600 3221220212 134563134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28896 26690 145 145 0 28751 0
[pid=11156] vsize: 115584
Current children cumulated CPU time (s) 468.57
Current children cumulated vsize (Kb) 119780

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.85 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61128 0 0 0 47661 195 0 0 25 0 1 0 1736702649 118415360 26705 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28910 26705 145 145 0 28765 0
[pid=11156] vsize: 115640
Current children cumulated CPU time (s) 478.57
Current children cumulated vsize (Kb) 119836

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61149 0 0 0 48660 195 0 0 25 0 1 0 1736702649 118497280 26726 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 28930 26726 145 145 0 28785 0
[pid=11156] vsize: 115720
Current children cumulated CPU time (s) 488.56
Current children cumulated vsize (Kb) 119916

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61162 0 0 0 49660 195 0 0 25 0 1 0 1736702649 118550528 26739 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28943 26739 145 145 0 28798 0
[pid=11156] vsize: 115772
Current children cumulated CPU time (s) 498.56
Current children cumulated vsize (Kb) 119968

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61187 0 0 0 50660 196 0 0 25 0 1 0 1736702649 118648832 26764 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28967 26764 145 145 0 28822 0
[pid=11156] vsize: 115868
Current children cumulated CPU time (s) 508.57
Current children cumulated vsize (Kb) 120064

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61211 0 0 0 51659 196 0 0 25 0 1 0 1736702649 118743040 26788 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 28990 26788 145 145 0 28845 0
[pid=11156] vsize: 115960
Current children cumulated CPU time (s) 518.56
Current children cumulated vsize (Kb) 120156

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61559 0 0 0 52653 199 0 0 25 0 1 0 1736702649 120131584 27136 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 29329 27136 145 145 0 29184 0
[pid=11156] vsize: 117316
Current children cumulated CPU time (s) 528.53
Current children cumulated vsize (Kb) 121512

[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61912 0 0 0 53647 201 0 0 25 0 1 0 1736702649 121581568 27489 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 29683 27489 145 145 0 29538 0
[pid=11156] vsize: 118732
Current children cumulated CPU time (s) 538.49
Current children cumulated vsize (Kb) 122928

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61925 0 0 0 54647 201 0 0 25 0 1 0 1736702649 121630720 27502 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 29695 27502 145 145 0 29550 0
[pid=11156] vsize: 118780
Current children cumulated CPU time (s) 548.49
Current children cumulated vsize (Kb) 122976

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 61966 0 0 0 55647 201 0 0 25 0 1 0 1736702649 121790464 27543 4294967295 134512640 135094434 3221221600 3221220260 134562166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 29734 27543 145 145 0 29589 0
[pid=11156] vsize: 118936
Current children cumulated CPU time (s) 558.49
Current children cumulated vsize (Kb) 123132

[startup+570.05 s]
Raw data (loadavg): 0.99 0.97 0.86 1/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) T 11152 11152 10120 0 -1 0 62053 0 0 0 56646 202 0 0 25 0 1 0 1736702649 122134528 27630 4294967295 134512640 135094434 3221221600 3221219980 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/11156/statm): 29818 27630 145 145 0 29673 0
[pid=11156] vsize: 119272
Current children cumulated CPU time (s) 568.49
Current children cumulated vsize (Kb) 123468

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.86 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 62518 0 0 0 57638 205 0 0 25 0 1 0 1736702649 124264448 28095 4294967295 134512640 135094434 3221221600 3221220256 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30338 28095 145 145 0 30193 0
[pid=11156] vsize: 121352
Current children cumulated CPU time (s) 578.44
Current children cumulated vsize (Kb) 125548

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 62827 0 0 0 58633 207 0 0 25 0 1 0 1736702649 125509632 28404 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30642 28404 145 145 0 30497 0
[pid=11156] vsize: 122568
Current children cumulated CPU time (s) 588.41
Current children cumulated vsize (Kb) 126764

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63036 0 0 0 59630 208 0 0 25 0 1 0 1736702649 126365696 28613 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30851 28613 145 145 0 30706 0
[pid=11156] vsize: 123404
Current children cumulated CPU time (s) 598.39
Current children cumulated vsize (Kb) 127600

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63071 0 0 0 60630 209 0 0 25 0 1 0 1736702649 126504960 28648 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30885 28648 145 145 0 30740 0
[pid=11156] vsize: 123540
Current children cumulated CPU time (s) 608.4
Current children cumulated vsize (Kb) 127736

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63104 0 0 0 61630 209 0 0 25 0 1 0 1736702649 126656512 28681 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30922 28681 145 145 0 30777 0
[pid=11156] vsize: 123688
Current children cumulated CPU time (s) 618.4
Current children cumulated vsize (Kb) 127884

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63138 0 0 0 62629 209 0 0 25 0 1 0 1736702649 126787584 28715 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30954 28715 145 145 0 30809 0
[pid=11156] vsize: 123816
Current children cumulated CPU time (s) 628.39
Current children cumulated vsize (Kb) 128012

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63159 0 0 0 63628 210 0 0 25 0 1 0 1736702649 126881792 28736 4294967295 134512640 135094434 3221221600 3221220240 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30977 28736 145 145 0 30832 0
[pid=11156] vsize: 123908
Current children cumulated CPU time (s) 638.39
Current children cumulated vsize (Kb) 128104

[startup+650.055 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63174 0 0 0 64628 211 0 0 25 0 1 0 1736702649 126943232 28751 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 30992 28751 145 145 0 30847 0
[pid=11156] vsize: 123968
Current children cumulated CPU time (s) 648.4
Current children cumulated vsize (Kb) 128164

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63192 0 0 0 65628 212 0 0 25 0 1 0 1736702649 127008768 28769 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31008 28769 145 145 0 30863 0
[pid=11156] vsize: 124032
Current children cumulated CPU time (s) 658.41
Current children cumulated vsize (Kb) 128228

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63214 0 0 0 66627 212 0 0 25 0 1 0 1736702649 127107072 28791 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31032 28791 145 145 0 30887 0
[pid=11156] vsize: 124128
Current children cumulated CPU time (s) 668.4
Current children cumulated vsize (Kb) 128324

[startup+680.058 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63251 0 0 0 67627 213 0 0 25 0 1 0 1736702649 127250432 28828 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31067 28828 145 145 0 30922 0
[pid=11156] vsize: 124268
Current children cumulated CPU time (s) 678.41
Current children cumulated vsize (Kb) 128464

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.87 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63269 0 0 0 68627 213 0 0 25 0 1 0 1736702649 127320064 28846 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31084 28846 145 145 0 30939 0
[pid=11156] vsize: 124336
Current children cumulated CPU time (s) 688.41
Current children cumulated vsize (Kb) 128532

[startup+700.059 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63287 0 0 0 69627 213 0 0 25 0 1 0 1736702649 127389696 28864 4294967295 134512640 135094434 3221221600 3221220256 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31101 28864 145 145 0 30956 0
[pid=11156] vsize: 124404
Current children cumulated CPU time (s) 698.41
Current children cumulated vsize (Kb) 128600

[startup+710.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63310 0 0 0 70626 213 0 0 25 0 1 0 1736702649 127483904 28887 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31124 28887 145 145 0 30979 0
[pid=11156] vsize: 124496
Current children cumulated CPU time (s) 708.4
Current children cumulated vsize (Kb) 128692

[startup+720.06 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63328 0 0 0 71626 214 0 0 25 0 1 0 1736702649 127545344 28905 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31139 28905 145 145 0 30994 0
[pid=11156] vsize: 124556
Current children cumulated CPU time (s) 718.41
Current children cumulated vsize (Kb) 128752

[startup+730.061 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63350 0 0 0 72626 214 0 0 25 0 1 0 1736702649 127631360 28927 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31160 28927 145 145 0 31015 0
[pid=11156] vsize: 124640
Current children cumulated CPU time (s) 728.41
Current children cumulated vsize (Kb) 128836

[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63365 0 0 0 73626 214 0 0 25 0 1 0 1736702649 127688704 28942 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31174 28942 145 145 0 31029 0
[pid=11156] vsize: 124696
Current children cumulated CPU time (s) 738.41
Current children cumulated vsize (Kb) 128892

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63376 0 0 0 74626 215 0 0 25 0 1 0 1736702649 127733760 28953 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31185 28953 145 145 0 31040 0
[pid=11156] vsize: 124740
Current children cumulated CPU time (s) 748.42
Current children cumulated vsize (Kb) 128936

[startup+760.064 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63389 0 0 0 75626 215 0 0 25 0 1 0 1736702649 127782912 28966 4294967295 134512640 135094434 3221221600 3221220256 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31197 28966 145 145 0 31052 0
[pid=11156] vsize: 124788
Current children cumulated CPU time (s) 758.42
Current children cumulated vsize (Kb) 128984

[startup+770.064 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63396 0 0 0 76626 215 0 0 25 0 1 0 1736702649 127811584 28973 4294967295 134512640 135094434 3221221600 3221220224 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31204 28973 145 145 0 31059 0
[pid=11156] vsize: 124816
Current children cumulated CPU time (s) 768.42
Current children cumulated vsize (Kb) 129012

[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63408 0 0 0 77625 215 0 0 25 0 1 0 1736702649 127852544 28985 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31214 28985 145 145 0 31069 0
[pid=11156] vsize: 124856
Current children cumulated CPU time (s) 778.41
Current children cumulated vsize (Kb) 129052

[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.88 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63424 0 0 0 78625 216 0 0 25 0 1 0 1736702649 127913984 29001 4294967295 134512640 135094434 3221221600 3221220232 134562981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31229 29001 145 145 0 31084 0
[pid=11156] vsize: 124916
Current children cumulated CPU time (s) 788.42
Current children cumulated vsize (Kb) 129112

[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63440 0 0 0 79625 216 0 0 25 0 1 0 1736702649 127979520 29017 4294967295 134512640 135094434 3221221600 3221220256 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31245 29017 145 145 0 31100 0
[pid=11156] vsize: 124980
Current children cumulated CPU time (s) 798.42
Current children cumulated vsize (Kb) 129176

[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63452 0 0 0 80625 216 0 0 25 0 1 0 1736702649 128028672 29029 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31257 29029 145 145 0 31112 0
[pid=11156] vsize: 125028
Current children cumulated CPU time (s) 808.42
Current children cumulated vsize (Kb) 129224

[startup+820.068 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63462 0 0 0 81625 216 0 0 25 0 1 0 1736702649 128065536 29039 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31266 29039 145 145 0 31121 0
[pid=11156] vsize: 125064
Current children cumulated CPU time (s) 818.42
Current children cumulated vsize (Kb) 129260

[startup+830.069 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63478 0 0 0 82624 217 0 0 25 0 1 0 1736702649 128126976 29055 4294967295 134512640 135094434 3221221600 3221220260 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31281 29055 145 145 0 31136 0
[pid=11156] vsize: 125124
Current children cumulated CPU time (s) 828.42
Current children cumulated vsize (Kb) 129320

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63498 0 0 0 83624 217 0 0 25 0 1 0 1736702649 128204800 29075 4294967295 134512640 135094434 3221221600 3221220256 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31300 29075 145 145 0 31155 0
[pid=11156] vsize: 125200
Current children cumulated CPU time (s) 838.42
Current children cumulated vsize (Kb) 129396

[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63510 0 0 0 84624 217 0 0 25 0 1 0 1736702649 128249856 29087 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31311 29087 145 145 0 31166 0
[pid=11156] vsize: 125244
Current children cumulated CPU time (s) 848.42
Current children cumulated vsize (Kb) 129440

[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63522 0 0 0 85624 217 0 0 25 0 1 0 1736702649 128299008 29099 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31323 29099 145 145 0 31178 0
[pid=11156] vsize: 125292
Current children cumulated CPU time (s) 858.42
Current children cumulated vsize (Kb) 129488

[startup+870.072 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63534 0 0 0 86624 217 0 0 25 0 1 0 1736702649 128344064 29111 4294967295 134512640 135094434 3221221600 3221220212 134563094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31334 29111 145 145 0 31189 0
[pid=11156] vsize: 125336
Current children cumulated CPU time (s) 868.42
Current children cumulated vsize (Kb) 129532

[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63549 0 0 0 87624 218 0 0 25 0 1 0 1736702649 128401408 29126 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31348 29126 145 145 0 31203 0
[pid=11156] vsize: 125392
Current children cumulated CPU time (s) 878.43
Current children cumulated vsize (Kb) 129588

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.89 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63558 0 0 0 88624 218 0 0 25 0 1 0 1736702649 128438272 29135 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31357 29135 145 145 0 31212 0
[pid=11156] vsize: 125428
Current children cumulated CPU time (s) 888.43
Current children cumulated vsize (Kb) 129624

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63581 0 0 0 89624 218 0 0 25 0 1 0 1736702649 128532480 29158 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31380 29158 145 145 0 31235 0
[pid=11156] vsize: 125520
Current children cumulated CPU time (s) 898.43
Current children cumulated vsize (Kb) 129716

[startup+910.076 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63595 0 0 0 90624 218 0 0 25 0 1 0 1736702649 128585728 29172 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31393 29172 145 145 0 31248 0
[pid=11156] vsize: 125572
Current children cumulated CPU time (s) 908.43
Current children cumulated vsize (Kb) 129768

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63622 0 0 0 91624 218 0 0 25 0 1 0 1736702649 128659456 29199 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31411 29199 145 145 0 31266 0
[pid=11156] vsize: 125644
Current children cumulated CPU time (s) 918.43
Current children cumulated vsize (Kb) 129840

[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63640 0 0 0 92623 218 0 0 25 0 1 0 1736702649 128729088 29217 4294967295 134512640 135094434 3221221600 3221220256 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31428 29217 145 145 0 31283 0
[pid=11156] vsize: 125712
Current children cumulated CPU time (s) 928.42
Current children cumulated vsize (Kb) 129908

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63657 0 0 0 93623 218 0 0 25 0 1 0 1736702649 128798720 29234 4294967295 134512640 135094434 3221221600 3221220256 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31445 29234 145 145 0 31300 0
[pid=11156] vsize: 125780
Current children cumulated CPU time (s) 938.42
Current children cumulated vsize (Kb) 129976

[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63676 0 0 0 94623 219 0 0 25 0 1 0 1736702649 128872448 29253 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31463 29253 145 145 0 31318 0
[pid=11156] vsize: 125852
Current children cumulated CPU time (s) 948.43
Current children cumulated vsize (Kb) 130048

[startup+960.08 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63692 0 0 0 95623 219 0 0 25 0 1 0 1736702649 128933888 29269 4294967295 134512640 135094434 3221221600 3221220212 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31478 29269 145 145 0 31333 0
[pid=11156] vsize: 125912
Current children cumulated CPU time (s) 958.43
Current children cumulated vsize (Kb) 130108

[startup+970.081 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63707 0 0 0 96623 219 0 0 25 0 1 0 1736702649 128991232 29284 4294967295 134512640 135094434 3221221600 3221220240 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31492 29284 145 145 0 31347 0
[pid=11156] vsize: 125968
Current children cumulated CPU time (s) 968.43
Current children cumulated vsize (Kb) 130164

[startup+980.082 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63741 0 0 0 97623 219 0 0 25 0 1 0 1736702649 129138688 29318 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31528 29318 145 145 0 31383 0
[pid=11156] vsize: 126112
Current children cumulated CPU time (s) 978.43
Current children cumulated vsize (Kb) 130308

[startup+990.083 s]
Raw data (loadavg): 0.99 0.97 0.90 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63774 0 0 0 98622 220 0 0 25 0 1 0 1736702649 129269760 29351 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31560 29351 145 145 0 31415 0
[pid=11156] vsize: 126240
Current children cumulated CPU time (s) 988.43
Current children cumulated vsize (Kb) 130436

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63788 0 0 0 99622 220 0 0 25 0 1 0 1736702649 129323008 29365 4294967295 134512640 135094434 3221221600 3221220256 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31573 29365 145 145 0 31428 0
[pid=11156] vsize: 126292
Current children cumulated CPU time (s) 998.43
Current children cumulated vsize (Kb) 130488

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63813 0 0 0 100622 220 0 0 25 0 1 0 1736702649 129421312 29390 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31597 29390 145 145 0 31452 0
[pid=11156] vsize: 126388
Current children cumulated CPU time (s) 1008.43
Current children cumulated vsize (Kb) 130584

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63840 0 0 0 101621 221 0 0 25 0 1 0 1736702649 129527808 29417 4294967295 134512640 135094434 3221221600 3221220240 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31623 29417 145 145 0 31478 0
[pid=11156] vsize: 126492
Current children cumulated CPU time (s) 1018.43
Current children cumulated vsize (Kb) 130688

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63855 0 0 0 102621 221 0 0 25 0 1 0 1736702649 129585152 29432 4294967295 134512640 135094434 3221221600 3221220288 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31637 29432 145 145 0 31492 0
[pid=11156] vsize: 126548
Current children cumulated CPU time (s) 1028.43
Current children cumulated vsize (Kb) 130744

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63871 0 0 0 103621 221 0 0 25 0 1 0 1736702649 129650688 29448 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31653 29448 145 145 0 31508 0
[pid=11156] vsize: 126612
Current children cumulated CPU time (s) 1038.43
Current children cumulated vsize (Kb) 130808

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63884 0 0 0 104621 221 0 0 25 0 1 0 1736702649 129699840 29461 4294967295 134512640 135094434 3221221600 3221220256 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31665 29461 145 145 0 31520 0
[pid=11156] vsize: 126660
Current children cumulated CPU time (s) 1048.43
Current children cumulated vsize (Kb) 130856

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11156
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63898 0 0 0 105621 221 0 0 25 0 1 0 1736702649 129753088 29475 4294967295 134512640 135094434 3221221600 3221220256 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31678 29475 145 145 0 31533 0
[pid=11156] vsize: 126712
Current children cumulated CPU time (s) 1058.43
Current children cumulated vsize (Kb) 130908

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63913 0 0 0 106621 221 0 0 25 0 1 0 1736702649 129814528 29490 4294967295 134512640 135094434 3221221600 3221220256 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31693 29490 145 145 0 31548 0
[pid=11156] vsize: 126772
Current children cumulated CPU time (s) 1068.43
Current children cumulated vsize (Kb) 130968

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63927 0 0 0 107621 221 0 0 25 0 1 0 1736702649 129867776 29504 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31706 29504 145 145 0 31561 0
[pid=11156] vsize: 126824
Current children cumulated CPU time (s) 1078.43
Current children cumulated vsize (Kb) 131020

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63939 0 0 0 108621 222 0 0 25 0 1 0 1736702649 129916928 29516 4294967295 134512640 135094434 3221221600 3221220256 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31718 29516 145 145 0 31573 0
[pid=11156] vsize: 126872
Current children cumulated CPU time (s) 1088.44
Current children cumulated vsize (Kb) 131068

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63963 0 0 0 109620 222 0 0 25 0 1 0 1736702649 130007040 29540 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31740 29540 145 145 0 31595 0
[pid=11156] vsize: 126960
Current children cumulated CPU time (s) 1098.43
Current children cumulated vsize (Kb) 131156

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 63990 0 0 0 110620 222 0 0 25 0 1 0 1736702649 130101248 29567 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31763 29567 145 145 0 31618 0
[pid=11156] vsize: 127052
Current children cumulated CPU time (s) 1108.43
Current children cumulated vsize (Kb) 131248

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64002 0 0 0 111621 222 0 0 25 0 1 0 1736702649 130150400 29579 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31775 29579 145 145 0 31630 0
[pid=11156] vsize: 127100
Current children cumulated CPU time (s) 1118.44
Current children cumulated vsize (Kb) 131296

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64023 0 0 0 112620 222 0 0 25 0 1 0 1736702649 130232320 29600 4294967295 134512640 135094434 3221221600 3221220212 134563085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31795 29600 145 145 0 31650 0
[pid=11156] vsize: 127180
Current children cumulated CPU time (s) 1128.43
Current children cumulated vsize (Kb) 131376

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64032 0 0 0 113620 222 0 0 25 0 1 0 1736702649 130269184 29609 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31804 29609 145 145 0 31659 0
[pid=11156] vsize: 127216
Current children cumulated CPU time (s) 1138.43
Current children cumulated vsize (Kb) 131412

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64042 0 0 0 114620 223 0 0 25 0 1 0 1736702649 130830336 29619 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31941 29619 145 145 0 31796 0
[pid=11156] vsize: 127764
Current children cumulated CPU time (s) 1148.44
Current children cumulated vsize (Kb) 131960

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64054 0 0 0 115620 223 0 0 25 0 1 0 1736702649 130875392 29631 4294967295 134512640 135094434 3221221600 3221220256 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31952 29631 145 145 0 31807 0
[pid=11156] vsize: 127808
Current children cumulated CPU time (s) 1158.44
Current children cumulated vsize (Kb) 132004

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64066 0 0 0 116620 223 0 0 25 0 1 0 1736702649 130924544 29643 4294967295 134512640 135094434 3221221600 3221220236 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31964 29643 145 145 0 31819 0
[pid=11156] vsize: 127856
Current children cumulated CPU time (s) 1168.44
Current children cumulated vsize (Kb) 132052

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64077 0 0 0 117619 224 0 0 25 0 1 0 1736702649 130965504 29654 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11156/statm): 31974 29654 145 145 0 31829 0
[pid=11156] vsize: 127896
Current children cumulated CPU time (s) 1178.44
Current children cumulated vsize (Kb) 132092

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64091 0 0 0 118619 224 0 0 25 0 1 0 1736702649 131022848 29668 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 31988 29668 145 145 0 31843 0
[pid=11156] vsize: 127952
Current children cumulated CPU time (s) 1188.44
Current children cumulated vsize (Kb) 132148

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64104 0 0 0 119619 224 0 0 25 0 1 0 1736702649 131076096 29681 4294967295 134512640 135094434 3221221600 3221220212 134563092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 32001 29681 145 145 0 31856 0
[pid=11156] vsize: 128004
Current children cumulated CPU time (s) 1198.44
Current children cumulated vsize (Kb) 132200

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64114 0 0 0 120619 224 0 0 25 0 1 0 1736702649 131117056 29691 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 32011 29691 145 145 0 31866 0
[pid=11156] vsize: 128044
Current children cumulated CPU time (s) 1208.44
Current children cumulated vsize (Kb) 132240



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11158
Raw data (/proc/11152/stat): 11152 (minisat+_script) S 11151 11152 10120 0 -1 0 322 276 0 0 0 0 0 1 21 0 1 0 1736702643 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11152/statm): 1049 256 1003 147 0 902 0
[pid=11152] vsize: 4196
Raw data (/proc/11156/stat): 11156 (minisat+_64-bit) R 11152 11152 10120 0 -1 0 64114 0 0 0 120619 224 0 0 25 0 1 0 1736702649 131117056 29691 4294967295 134512640 135094434 3221221600 3221220212 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11156/statm): 32011 29691 145 145 0 31866 0
[pid=11156] vsize: 128044
Current children cumulated CPU time (s) 1208.44
Current children cumulated vsize (Kb) 132240

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.5
CPU user time (s): 1206.19
CPU system time (s): 2.30365
CPU usage (%): 99.8624
Max. virtual memory (cumulated for all children) (Kb): 132240

Verifier Data

ERROR: no interpretation found !