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-t1717.opb
MD5SUMbc46e72682d969c09e6f4028df473a45
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 201342
Optimality of the best value was proved NO
Number of terms in the objective function 73885
Biggest coefficient in the objective function 4066
Number of bits for the biggest coefficient in the objective function 12
Sum of the numbers in the objective function 172074995
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 4066
Number of bits of the biggest number in a constraint 12
Biggest sum of numbers in a constraint 172074995
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1191.77
Number of variables73885
Total number of constraints74436
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)74436
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint612

Trace number 4489

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        870672 kB
Buffers:         36160 kB
Cached:          99960 kB
SwapCached:        832 kB
Active:          83028 kB
Inactive:        55740 kB
HighTotal:      131008 kB
HighFree:        30268 kB
LowTotal:       903652 kB
LowFree:        840404 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            19640 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:02:10 (client local time) WITH STATUS 0 IN 1207.03 SECONDS
stats: 2946 7 1207.03 0

Solver Data

c Parsing PB file...
c Converting 1102 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1100]---> BDD-cost: 1179
c ---[1098]---> BDD-cost: 1181
c ---[1096]---> BDD-cost: 1169
c ---[1094]---> BDD-cost: 1171
c ---[1092]---> BDD-cost: 1183
c ---[1090]---> BDD-cost: 1167
c ---[1088]---> BDD-cost: 1169
c ---[1086]---> BDD-cost: 1181
c ---[1084]---> BDD-cost: 1177
c ---[1082]---> BDD-cost: 1175
c ---[1080]---> BDD-cost: 1183
c ---[1078]---> BDD-cost: 1179
c ---[1076]---> BDD-cost: 1175
c ---[1074]---> BDD-cost: 1171
c ---[1072]---> BDD-cost: 1167
c ---[1070]---> BDD-cost: 1169
c ---[1068]---> BDD-cost: 1167
c ---[1066]---> BDD-cost: 1189
c ---[1064]---> BDD-cost: 1167
c ---[1062]---> BDD-cost: 1169
c ---[1060]---> BDD-cost: 1179
c ---[1058]---> BDD-cost: 1173
c ---[1056]---> BDD-cost: 1215
c ---[1054]---> BDD-cost: 1167
c ---[1052]---> BDD-cost: 1179
c ---[1050]---> BDD-cost: 1173
c ---[1048]---> BDD-cost: 1181
c ---[1046]---> BDD-cost: 1191
c ---[1044]---> BDD-cost: 1175
c ---[1042]---> BDD-cost: 1173
c ---[1040]---> BDD-cost: 1171
c ---[1038]---> BDD-cost: 1177
c ---[1036]---> BDD-cost: 1169
c ---[1034]---> BDD-cost: 1169
c ---[1032]---> BDD-cost: 1187
c ---[1030]---> BDD-cost: 1187
c ---[1028]---> BDD-cost: 1169
c ---[1026]---> BDD-cost: 1175
c ---[1024]---> BDD-cost: 1179
c ---[1022]---> BDD-cost: 1177
c ---[1020]---> BDD-cost: 1171
c ---[1018]---> BDD-cost: 1175
c ---[1016]---> BDD-cost: 1187
c ---[1014]---> BDD-cost: 1179
c ---[1012]---> BDD-cost: 1187
c ---[1010]---> BDD-cost: 1169
c ---[1008]---> BDD-cost: 1183
c ---[1006]---> BDD-cost: 1185
c ---[1004]---> BDD-cost: 1175
c ---[1002]---> BDD-cost: 1179
c ---[1000]---> BDD-cost: 1181
c ---[ 998]---> BDD-cost: 1155
c ---[ 996]---> BDD-cost: 1203
c ---[ 994]---> BDD-cost: 1191
c ---[ 992]---> BDD-cost: 1189
c ---[ 990]---> BDD-cost: 1175
c ---[ 988]---> BDD-cost: 1171
c ---[ 986]---> BDD-cost: 1191
c ---[ 984]---> BDD-cost: 1169
c ---[ 982]---> BDD-cost: 1187
c ---[ 980]---> BDD-cost: 1027
c ---[ 978]---> BDD-cost: 1175
c ---[ 976]---> BDD-cost: 1039
c ---[ 974]---> BDD-cost: 1185
c ---[ 972]---> BDD-cost: 1177
c ---[ 970]---> BDD-cost: 1167
c ---[ 968]---> BDD-cost: 1175
c ---[ 966]---> BDD-cost: 1171
c ---[ 964]---> BDD-cost: 1171
c ---[ 962]---> BDD-cost: 1175
c ---[ 960]---> BDD-cost: 1193
c ---[ 958]---> BDD-cost: 1171
c ---[ 956]---> BDD-cost: 1193
c ---[ 954]---> BDD-cost: 1175
c ---[ 952]---> BDD-cost: 1029
c ---[ 950]---> BDD-cost: 1193
c ---[ 948]---> BDD-cost: 1103
c ---[ 946]---> BDD-cost: 1171
c ---[ 944]---> BDD-cost: 1189
c ---[ 942]---> BDD-cost: 1179
c ---[ 940]---> BDD-cost: 1191
c ---[ 938]---> BDD-cost: 1003
c ---[ 936]---> BDD-cost: 1171
c ---[ 934]---> BDD-cost: 1171
c ---[ 932]---> BDD-cost: 1213
c ---[ 930]---> BDD-cost: 1175
c ---[ 928]---> BDD-cost: 1181
c ---[ 926]---> BDD-cost: 1173
c ---[ 924]---> BDD-cost: 1179
c ---[ 922]---> BDD-cost: 1179
c ---[ 920]---> BDD-cost: 1175
c ---[ 918]---> BDD-cost:  989
c ---[ 916]---> BDD-cost: 1187
c ---[ 914]---> BDD-cost: 1025
c ---[ 912]---> BDD-cost: 1141
c ---[ 910]---> BDD-cost: 1167
c ---[ 908]---> BDD-cost: 1115
c ---[ 906]---> BDD-cost: 1187
c ---[ 904]---> BDD-cost: 1117
c ---[ 902]---> BDD-cost: 1075
c ---[ 900]---> BDD-cost: 1167
c ---[ 898]---> BDD-cost: 1017
c ---[ 896]---> BDD-cost: 1079
c ---[ 894]---> BDD-cost: 1179
c ---[ 892]---> BDD-cost: 1191
c ---[ 890]---> BDD-cost: 1181
c ---[ 888]---> BDD-cost: 1171
c ---[ 886]---> BDD-cost: 1189
c ---[ 884]---> BDD-cost: 1177
c ---[ 882]---> BDD-cost: 1159
c ---[ 880]---> BDD-cost: 1181
c ---[ 878]---> BDD-cost: 1169
c ---[ 876]---> BDD-cost: 1167
c ---[ 874]---> BDD-cost: 1027
c ---[ 872]---> BDD-cost: 1093
c ---[ 870]---> BDD-cost: 1195
c ---[ 868]---> BDD-cost: 1169
c ---[ 866]---> BDD-cost: 1173
c ---[ 864]---> BDD-cost: 1171
c ---[ 862]---> BDD-cost: 1151
c ---[ 860]---> BDD-cost: 1173
c ---[ 858]---> BDD-cost: 1155
c ---[ 856]---> BDD-cost: 1173
c ---[ 854]---> BDD-cost: 1171
c ---[ 852]---> BDD-cost: 1145
c ---[ 850]---> BDD-cost: 1177
c ---[ 848]---> BDD-cost: 1179
c ---[ 846]---> BDD-cost: 1173
c ---[ 844]---> BDD-cost: 1173
c ---[ 842]---> BDD-cost: 1173
c ---[ 840]---> BDD-cost: 1187
c ---[ 838]---> BDD-cost: 1169
c ---[ 836]---> BDD-cost: 1055
c ---[ 834]---> BDD-cost: 1121
c ---[ 832]---> BDD-cost: 1171
c ---[ 830]---> BDD-cost: 1173
c ---[ 828]---> BDD-cost: 1177
c ---[ 826]---> BDD-cost: 1169
c ---[ 824]---> BDD-cost: 1171
c ---[ 822]---> BDD-cost: 1173
c ---[ 820]---> BDD-cost: 1169
c ---[ 818]---> BDD-cost: 1201
c ---[ 816]---> BDD-cost: 1173
c ---[ 814]---> BDD-cost: 1097
c ---[ 812]---> BDD-cost: 1171
c ---[ 810]---> BDD-cost: 1161
c ---[ 808]---> BDD-cost: 1187
c ---[ 806]---> BDD-cost: 1131
c ---[ 804]---> BDD-cost: 1173
c ---[ 802]---> BDD-cost: 1175
c ---[ 800]---> BDD-cost: 1171
c ---[ 798]---> BDD-cost: 1171
c ---[ 796]---> BDD-cost: 1169
c ---[ 794]---> BDD-cost: 1169
c ---[ 792]---> BDD-cost: 1165
c ---[ 790]---> BDD-cost: 1177
c ---[ 788]---> BDD-cost: 1157
c ---[ 786]---> BDD-cost: 1179
c ---[ 784]---> BDD-cost: 1129
c ---[ 782]---> BDD-cost: 1173
c ---[ 780]---> BDD-cost: 1175
c ---[ 778]---> BDD-cost: 1179
c ---[ 776]---> BDD-cost: 1173
c ---[ 774]---> BDD-cost: 1115
c ---[ 772]---> BDD-cost: 1071
c ---[ 770]---> BDD-cost: 1167
c ---[ 768]---> BDD-cost: 1187
c ---[ 766]---> BDD-cost: 1173
c ---[ 764]---> BDD-cost: 1091
c ---[ 762]---> BDD-cost: 1169
c ---[ 760]---> BDD-cost: 1025
c ---[ 758]---> BDD-cost: 1073
c ---[ 756]---> BDD-cost: 1167
c ---[ 754]---> BDD-cost: 1077
c ---[ 752]---> BDD-cost: 1197
c ---[ 750]---> BDD-cost: 1189
c ---[ 748]---> BDD-cost: 1197
c ---[ 746]---> BDD-cost: 1131
c ---[ 744]---> BDD-cost: 1115
c ---[ 742]---> BDD-cost: 1189
c ---[ 740]---> BDD-cost: 1177
c ---[ 738]---> BDD-cost: 1167
c ---[ 736]---> BDD-cost: 1175
c ---[ 734]---> BDD-cost: 1181
c ---[ 732]---> BDD-cost: 1171
c ---[ 730]---> BDD-cost: 1171
c ---[ 728]---> BDD-cost: 1189
c ---[ 726]---> BDD-cost: 1191
c ---[ 724]---> BDD-cost: 1103
c ---[ 722]---> BDD-cost: 1183
c ---[ 720]---> BDD-cost: 1151
c ---[ 718]---> BDD-cost: 1103
c ---[ 716]---> BDD-cost: 1171
c ---[ 714]---> BDD-cost: 1183
c ---[ 712]---> BDD-cost: 1171
c ---[ 710]---> BDD-cost: 1179
c ---[ 708]---> BDD-cost: 1173
c ---[ 706]---> BDD-cost: 1073
c ---[ 704]---> BDD-cost: 1191
c ---[ 702]---> BDD-cost: 1175
c ---[ 700]---> BDD-cost: 1139
c ---[ 698]---> BDD-cost: 1171
c ---[ 696]---> BDD-cost: 1173
c ---[ 694]---> BDD-cost: 1163
c ---[ 692]---> BDD-cost: 1173
c ---[ 690]---> BDD-cost: 1175
c ---[ 688]---> BDD-cost: 1189
c ---[ 686]---> BDD-cost: 1173
c ---[ 684]---> BDD-cost: 1173
c ---[ 682]---> BDD-cost: 1071
c ---[ 680]---> BDD-cost: 1179
c ---[ 678]---> BDD-cost: 1125
c ---[ 676]---> BDD-cost: 1171
c ---[ 674]---> BDD-cost: 1057
c ---[ 672]---> BDD-cost: 1189
c ---[ 670]---> BDD-cost: 1107
c ---[ 668]---> BDD-cost: 1159
c ---[ 666]---> BDD-cost: 1175
c ---[ 664]---> BDD-cost: 1063
c ---[ 662]---> BDD-cost: 1173
c ---[ 660]---> BDD-cost: 1171
c ---[ 658]---> BDD-cost: 1171
c ---[ 656]---> BDD-cost: 1165
c ---[ 654]---> BDD-cost: 1165
c ---[ 652]---> BDD-cost: 1171
c ---[ 650]---> BDD-cost: 1077
c ---[ 648]---> BDD-cost: 1069
c ---[ 646]---> BDD-cost: 1175
c ---[ 644]---> BDD-cost: 1159
c ---[ 642]---> BDD-cost: 1097
c ---[ 640]---> BDD-cost: 1175
c ---[ 638]---> BDD-cost:  859
c ---[ 636]---> BDD-cost: 1173
c ---[ 634]---> BDD-cost: 1169
c ---[ 632]---> BDD-cost: 1173
c ---[ 630]---> BDD-cost: 1097
c ---[ 628]---> BDD-cost: 1161
c ---[ 626]---> BDD-cost: 1157
c ---[ 624]---> BDD-cost: 1165
c ---[ 622]---> BDD-cost: 1185
c ---[ 620]---> BDD-cost: 1179
c ---[ 618]---> BDD-cost: 1155
c ---[ 616]---> BDD-cost: 1167
c ---[ 614]---> BDD-cost: 1181
c ---[ 612]---> BDD-cost: 1121
c ---[ 610]---> BDD-cost: 1121
c ---[ 608]---> BDD-cost:  963
c ---[ 606]---> BDD-cost: 1173
c ---[ 604]---> BDD-cost: 1151
c ---[ 602]---> BDD-cost: 1177
c ---[ 600]---> BDD-cost: 1191
c ---[ 598]---> BDD-cost: 1187
c ---[ 596]---> BDD-cost: 1051
c ---[ 594]---> BDD-cost:  987
c ---[ 592]---> BDD-cost: 1173
c ---[ 590]---> BDD-cost: 1175
c ---[ 588]---> BDD-cost: 1173
c ---[ 586]---> BDD-cost: 1121
c ---[ 584]---> BDD-cost: 1157
c ---[ 582]---> BDD-cost: 1173
c ---[ 580]---> BDD-cost: 1175
c ---[ 578]---> BDD-cost: 1181
c ---[ 576]---> BDD-cost: 1079
c ---[ 574]---> BDD-cost:  983
c ---[ 572]---> BDD-cost:  879
c ---[ 570]---> BDD-cost: 1169
c ---[ 568]---> BDD-cost: 1181
c ---[ 566]---> BDD-cost: 1169
c ---[ 564]---> BDD-cost: 1185
c ---[ 562]---> BDD-cost: 1177
c ---[ 560]---> BDD-cost: 1159
c ---[ 558]---> BDD-cost: 1153
c ---[ 556]---> BDD-cost: 1173
c ---[ 554]---> BDD-cost: 1191
c ---[ 552]---> BDD-cost: 1177
c ---[ 550]---> BDD-cost: 1175
c ---[ 548]---> BDD-cost:  887
c ---[ 546]---> BDD-cost: 1191
c ---[ 544]---> BDD-cost: 1155
c ---[ 542]---> BDD-cost: 1169
c ---[ 540]---> BDD-cost: 1127
c ---[ 538]---> BDD-cost: 1179
c ---[ 536]---> BDD-cost: 1189
c ---[ 534]---> BDD-cost: 1171
c ---[ 532]---> BDD-cost: 1167
c ---[ 530]---> BDD-cost: 1171
c ---[ 528]---> BDD-cost: 1175
c ---[ 526]---> BDD-cost:  885
c ---[ 524]---> BDD-cost: 1183
c ---[ 522]---> BDD-cost: 1175
c ---[ 520]---> BDD-cost: 1193
c ---[ 518]---> BDD-cost: 1181
c ---[ 516]---> BDD-cost: 1169
c ---[ 514]---> BDD-cost: 1181
c ---[ 512]---> BDD-cost: 1169
c ---[ 510]---> BDD-cost: 1177
c ---[ 508]---> BDD-cost: 1171
c ---[ 506]---> BDD-cost: 1169
c ---[ 504]---> BDD-cost: 1179
c ---[ 502]---> BDD-cost: 1183
c ---[ 500]---> BDD-cost: 1165
c ---[ 498]---> BDD-cost: 1163
c ---[ 496]---> BDD-cost: 1189
c ---[ 494]---> BDD-cost: 1181
c ---[ 492]---> BDD-cost: 1171
c ---[ 490]---> BDD-cost: 1171
c ---[ 488]---> BDD-cost: 1173
c ---[ 486]---> BDD-cost: 1171
c ---[ 484]---> BDD-cost: 1171
c ---[ 482]---> BDD-cost: 1175
c ---[ 480]---> BDD-cost: 1171
c ---[ 478]---> BDD-cost: 1141
c ---[ 476]---> BDD-cost: 1185
c ---[ 474]---> BDD-cost: 1167
c ---[ 472]---> BDD-cost: 1179
c ---[ 470]---> BDD-cost: 1175
c ---[ 468]---> BDD-cost: 1177
c ---[ 466]---> BDD-cost:  775
c ---[ 464]---> BDD-cost: 1191
c ---[ 462]---> BDD-cost: 1207
c ---[ 460]---> BDD-cost: 1179
c ---[ 458]---> BDD-cost: 1149
c ---[ 456]---> BDD-cost: 1183
c ---[ 454]---> BDD-cost:  787
c ---[ 452]---> BDD-cost: 1173
c ---[ 450]---> BDD-cost: 1169
c ---[ 448]---> BDD-cost: 1131
c ---[ 446]---> BDD-cost: 1129
c ---[ 444]---> BDD-cost: 1167
c ---[ 442]---> BDD-cost: 1177
c ---[ 440]---> BDD-cost: 1185
c ---[ 438]---> BDD-cost: 1185
c ---[ 436]---> BDD-cost: 1189
c ---[ 434]---> BDD-cost: 1169
c ---[ 432]---> BDD-cost: 1113
c ---[ 430]---> BDD-cost: 1167
c ---[ 428]---> BDD-cost: 1181
c ---[ 426]---> BDD-cost: 1171
c ---[ 424]---> BDD-cost: 1191
c ---[ 422]---> BDD-cost: 1181
c ---[ 420]---> BDD-cost: 1169
c ---[ 418]---> BDD-cost: 1137
c ---[ 416]---> BDD-cost: 1159
c ---[ 414]---> BDD-cost: 1169
c ---[ 412]---> BDD-cost: 1175
c ---[ 410]---> BDD-cost: 1167
c ---[ 408]---> BDD-cost: 1195
c ---[ 406]---> BDD-cost: 1169
c ---[ 404]---> BDD-cost: 1171
c ---[ 402]---> BDD-cost: 1177
c ---[ 400]---> BDD-cost: 1147
c ---[ 398]---> BDD-cost: 1171
c ---[ 396]---> BDD-cost: 1173
c ---[ 394]---> BDD-cost:  723
c ---[ 392]---> BDD-cost: 1173
c ---[ 390]---> BDD-cost: 1177
c ---[ 388]---> BDD-cost: 1169
c ---[ 386]---> BDD-cost: 1187
c ---[ 384]---> BDD-cost: 1209
c ---[ 382]---> BDD-cost: 1171
c ---[ 380]---> BDD-cost: 1181
c ---[ 378]---> BDD-cost: 1197
c ---[ 376]---> BDD-cost: 1183
c ---[ 374]---> BDD-cost: 1175
c ---[ 372]---> BDD-cost: 1165
c ---[ 370]---> BDD-cost: 1175
c ---[ 368]---> BDD-cost: 1175
c ---[ 366]---> BDD-cost: 1177
c ---[ 364]---> BDD-cost: 1179
c ---[ 362]---> BDD-cost: 1173
c ---[ 360]---> BDD-cost: 1169
c ---[ 358]---> BDD-cost: 1173
c ---[ 356]---> BDD-cost: 1173
c ---[ 354]---> BDD-cost: 1171
c ---[ 352]---> BDD-cost: 1177
c ---[ 350]---> BDD-cost: 1169
c ---[ 348]---> BDD-cost: 1185
c ---[ 346]---> BDD-cost: 1173
c ---[ 344]---> BDD-cost: 1103
c ---[ 342]---> BDD-cost: 1179
c ---[ 340]---> BDD-cost: 1173
c ---[ 338]---> BDD-cost: 1221
c ---[ 336]---> BDD-cost: 1177
c ---[ 334]---> BDD-cost: 1183
c ---[ 332]---> BDD-cost: 1179
c ---[ 330]---> BDD-cost: 1171
c ---[ 328]---> BDD-cost: 1175
c ---[ 326]---> BDD-cost: 1173
c ---[ 324]---> BDD-cost: 1175
c ---[ 322]---> BDD-cost: 1099
c ---[ 320]---> BDD-cost: 1203
c ---[ 318]---> BDD-cost: 1171
c ---[ 316]---> BDD-cost: 1165
c ---[ 314]---> BDD-cost: 1177
c ---[ 312]---> BDD-cost: 1169
c ---[ 310]---> BDD-cost: 1175
c ---[ 308]---> BDD-cost: 1173
c ---[ 306]---> BDD-cost: 1173
c ---[ 304]---> BDD-cost: 1183
c ---[ 302]---> BDD-cost: 1175
c ---[ 300]---> BDD-cost: 1165
c ---[ 298]---> BDD-cost: 1175
c ---[ 296]---> BDD-cost: 1153
c ---[ 294]---> BDD-cost: 1153
c ---[ 292]---> BDD-cost: 1175
c ---[ 290]---> BDD-cost: 1173
c ---[ 288]---> BDD-cost:  735
c ---[ 286]---> BDD-cost: 1179
c ---[ 284]---> BDD-cost: 1157
c ---[ 282]---> BDD-cost: 1183
c ---[ 280]---> BDD-cost: 1179
c ---[ 278]---> BDD-cost: 1181
c ---[ 276]---> BDD-cost: 1175
c ---[ 274]---> BDD-cost: 1181
c ---[ 272]---> BDD-cost: 1185
c ---[ 270]---> BDD-cost: 1161
c ---[ 268]---> BDD-cost: 1177
c ---[ 266]---> BDD-cost: 1165
c ---[ 264]---> BDD-cost: 1161
c ---[ 262]---> BDD-cost: 1065
c ---[ 260]---> BDD-cost: 1171
c ---[ 258]---> BDD-cost: 1189
c ---[ 256]---> BDD-cost: 1163
c ---[ 254]---> BDD-cost: 1177
c ---[ 252]---> BDD-cost: 1179
c ---[ 250]---> BDD-cost: 1187
c ---[ 248]---> BDD-cost: 1143
c ---[ 246]---> BDD-cost: 1183
c ---[ 244]---> BDD-cost: 1153
c ---[ 242]---> BDD-cost: 1177
c ---[ 240]---> BDD-cost: 1173
c ---[ 238]---> BDD-cost: 1177
c ---[ 236]---> BDD-cost: 1171
c ---[ 234]---> BDD-cost: 1103
c ---[ 232]---> BDD-cost: 1173
c ---[ 230]---> BDD-cost: 1175
c ---[ 228]---> BDD-cost: 1123
c ---[ 226]---> BDD-cost: 1169
c ---[ 224]---> BDD-cost: 1187
c ---[ 222]---> BDD-cost: 1101
c ---[ 220]---> BDD-cost: 1165
c ---[ 218]---> BDD-cost: 1193
c ---[ 216]---> BDD-cost: 1179
c ---[ 214]---> BDD-cost: 1177
c ---[ 212]---> BDD-cost: 1173
c ---[ 210]---> BDD-cost: 1173
c ---[ 208]---> BDD-cost: 1153
c ---[ 206]---> BDD-cost: 1183
c ---[ 204]---> BDD-cost: 1181
c ---[ 202]---> BDD-cost: 1179
c ---[ 200]---> BDD-cost: 1181
c ---[ 198]---> BDD-cost: 1181
c ---[ 196]---> BDD-cost: 1173
c ---[ 194]---> BDD-cost: 1173
c ---[ 192]---> BDD-cost: 1173
c ---[ 190]---> BDD-cost: 1185
c ---[ 188]---> BDD-cost: 1165
c ---[ 186]---> BDD-cost: 1173
c ---[ 184]---> BDD-cost: 1169
c ---[ 182]---> BDD-cost: 1183
c ---[ 180]---> BDD-cost: 1189
c ---[ 178]---> BDD-cost: 1177
c ---[ 176]---> BDD-cost: 1181
c ---[ 174]---> BDD-cost: 1173
c ---[ 172]---> BDD-cost: 1193
c ---[ 170]---> BDD-cost: 1173
c ---[ 168]---> BDD-cost: 1187
c ---[ 166]---> BDD-cost: 1193
c ---[ 164]---> BDD-cost: 1183
c ---[ 162]---> BDD-cost: 1175
c ---[ 160]---> BDD-cost: 1137
c ---[ 158]---> BDD-cost: 1185
c ---[ 156]---> BDD-cost: 1097
c ---[ 154]---> BDD-cost: 1195
c ---[ 152]---> BDD-cost: 1175
c ---[ 150]---> BDD-cost: 1175
c ---[ 148]---> BDD-cost: 1187
c ---[ 146]---> BDD-cost: 1179
c ---[ 144]---> BDD-cost: 1167
c ---[ 142]---> BDD-cost: 1175
c ---[ 140]---> BDD-cost: 1173
c ---[ 138]---> BDD-cost: 1173
c ---[ 136]---> BDD-cost: 1171
c ---[ 134]---> BDD-cost: 1179
c ---[ 132]---> BDD-cost: 1165
c ---[ 130]---> BDD-cost: 1165
c ---[ 128]---> BDD-cost: 1145
c ---[ 126]---> BDD-cost: 1179
c ---[ 124]---> BDD-cost: 1193
c ---[ 122]---> BDD-cost: 1175
c ---[ 120]---> BDD-cost: 1177
c ---[ 118]---> BDD-cost: 1181
c ---[ 116]---> BDD-cost: 1181
c ---[ 114]---> BDD-cost: 1195
c ---[ 112]---> BDD-cost: 1165
c ---[ 110]---> BDD-cost: 1169
c ---[ 108]---> BDD-cost: 1133
c ---[ 106]---> BDD-cost: 1199
c ---[ 104]---> BDD-cost: 1197
c ---[ 102]---> BDD-cost: 1177
c ---[ 100]---> BDD-cost: 1121
c ---[  98]---> BDD-cost: 1143
c ---[  96]---> BDD-cost: 1171
c ---[  94]---> BDD-cost: 1167
c ---[  92]---> BDD-cost: 1175
c ---[  90]---> BDD-cost: 1157
c ---[  88]---> BDD-cost: 1085
c ---[  86]---> BDD-cost: 1167
c ---[  84]---> BDD-cost: 1157
c ---[  82]---> BDD-cost: 1157
c ---[  80]---> BDD-cost: 1175
c ---[  78]---> BDD-cost: 1119
c ---[  76]---> BDD-cost: 1169
c ---[  74]---> BDD-cost: 1177
c ---[  72]---> BDD-cost: 1087
c ---[  70]---> BDD-cost: 1121
c ---[  68]---> BDD-cost: 1171
c ---[  66]---> BDD-cost: 1171
c ---[  64]---> BDD-cost: 1155
c ---[  62]---> BDD-cost: 1173
c ---[  60]---> BDD-cost: 1173
c ---[  58]---> BDD-cost: 1165
c ---[  56]---> BDD-cost: 1169
c ---[  54]---> BDD-cost: 1123
c ---[  52]---> BDD-cost: 1167
c ---[  50]---> BDD-cost: 1073
c ---[  48]---> BDD-cost: 1155
c ---[  46]---> BDD-cost: 1115
c ---[  44]---> BDD-cost: 1171
c ---[  42]---> BDD-cost: 1153
c ---[  40]---> BDD-cost: 1101
c ---[  38]---> BDD-cost: 1065
c ---[  36]---> BDD-cost: 1111
c ---[  34]---> BDD-cost: 1153
c ---[  32]---> BDD-cost: 1061
c ---[  30]---> BDD-cost: 1185
c ---[  28]---> BDD-cost: 1061
c ---[  26]---> BDD-cost: 1173
c ---[  24]---> BDD-cost: 1177
c ---[  22]---> BDD-cost: 1113
c ---[  20]---> BDD-cost: 1151
c ---[  18]---> BDD-cost: 1091
c ---[  16]---> BDD-cost: 1173
c ---[  14]---> BDD-cost: 1137
c ---[  12]---> BDD-cost: 1065
c ---[  10]---> BDD-cost: 1189
c ---[   8]---> BDD-cost: 1169
c ---[   6]---> BDD-cost: 1039
c ---[   4]---> BDD-cost: 1119
c ---[   2]---> BDD-cost: 1147
c ---[   0]---> BDD-cost: 1159
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1593441  4143559 |  531147       0        0     nan |  0.000 % |
c |       100 | 1593441  4143559 |  584261     100     3100    31.0 |  0.077 % |
c |       250 | 1593441  4143559 |  642687     250    15023    60.1 |  0.077 % |
c |       475 | 1593441  4143559 |  706956     475    28709    60.4 |  0.077 % |
c |       812 | 1593441  4143559 |  777652     812    75062    92.4 |  0.077 % |
c |      1329 | 1593441  4143559 |  855417    1329   184901   139.1 |  0.077 % |
c |      2088 | 1593441  4143559 |  940959    2088   283938   136.0 |  0.077 % |
c |      3228 | 1593441  4143559 | 1035055    3228   516925   160.1 |  0.077 % |
c |      4939 | 1593441  4143559 | 1138560    4939   851066   172.3 |  0.077 % |
c |      7501 | 1593441  4143559 | 1252416    7501  1448612   193.1 |  0.077 % |
c |     11345 | 1593441  4143559 | 1377658   11345  2447772   215.8 |  0.077 % |
c |     17111 | 1593441  4143559 | 1515424   17111  3892289   227.5 |  0.077 % |
c |     25761 | 1593441  4143559 | 1666966   25761  5900360   229.0 |  0.077 % |
c |     38735 | 1593441  4143559 | 1833663   38735  9114775   235.3 |  0.077 % |

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/24608/stat): 24608 (minisat+_script) R 24607 24608 5929 0 -1 0 19 0 0 0 0 0 0 0 19 0 1 0 1851762979 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24608/statm): 174 3 169 147 0 27 0
[pid=24608] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=24609
New process pid=24610
New process pid=24611
execve syscall for /bin/sed executable
One traced child (pid=24610) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=24611) exited with status: 0
One traced child (pid=24609) exited with status: 0
New process pid=24612
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-t1717.opb

[startup+10.005 s]
Raw data (loadavg): 0.88 0.94 0.69 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 13502 0 2 0 863 59 0 0 25 0 1 0 1851762984 55787520 12378 4294967295 134512640 135094434 3221224432 3221178112 134597040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 13620 12378 145 145 0 13475 0
[pid=24612] vsize: 54480
Current children cumulated CPU time (s) 9.23
Current children cumulated vsize (Kb) 56604

[startup+20.0058 s]
Raw data (loadavg): 0.90 0.94 0.69 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 28306 0 2 0 1759 112 0 0 20 0 1 0 1851762984 131080192 26523 4294967295 134512640 135094434 3221224432 3221145312 134538825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 32002 26523 145 145 0 31857 0
[pid=24612] vsize: 128008
Current children cumulated CPU time (s) 18.72
Current children cumulated vsize (Kb) 130132

[startup+30.0066 s]
Raw data (loadavg): 0.91 0.94 0.70 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 56731 0 2 0 2515 235 0 0 25 0 1 0 1851762984 259289088 54884 4294967295 134512640 135094434 3221224432 3221223056 134563167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 63303 54884 145 145 0 63158 0
[pid=24612] vsize: 253212
Current children cumulated CPU time (s) 27.51
Current children cumulated vsize (Kb) 255336

[startup+40.0083 s]
Raw data (loadavg): 0.93 0.94 0.70 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 56935 0 2 0 3512 236 0 0 25 0 1 0 1851762984 259420160 55088 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63335 55088 145 145 0 63190 0
[pid=24612] vsize: 253340
Current children cumulated CPU time (s) 37.49
Current children cumulated vsize (Kb) 255464

[startup+50.0091 s]
Raw data (loadavg): 0.94 0.95 0.70 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 56986 0 2 0 4511 237 0 0 25 0 1 0 1851762984 259624960 55139 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63385 55139 145 145 0 63240 0
[pid=24612] vsize: 253540
Current children cumulated CPU time (s) 47.49
Current children cumulated vsize (Kb) 255664

[startup+60.0099 s]
Raw data (loadavg): 0.95 0.95 0.71 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57046 0 2 0 5511 237 0 0 25 0 1 0 1851762984 259870720 55199 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63445 55199 145 145 0 63300 0
[pid=24612] vsize: 253780
Current children cumulated CPU time (s) 57.49
Current children cumulated vsize (Kb) 255904

[startup+70.0107 s]
Raw data (loadavg): 0.95 0.95 0.71 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57122 0 2 0 6509 237 0 0 25 0 1 0 1851762984 260182016 55275 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63521 55275 145 145 0 63376 0
[pid=24612] vsize: 254084
Current children cumulated CPU time (s) 67.47
Current children cumulated vsize (Kb) 256208

[startup+80.0114 s]
Raw data (loadavg): 0.96 0.95 0.71 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57175 0 2 0 7508 238 0 0 25 0 1 0 1851762984 260399104 55328 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63574 55328 145 145 0 63429 0
[pid=24612] vsize: 254296
Current children cumulated CPU time (s) 77.47
Current children cumulated vsize (Kb) 256420

[startup+90.0122 s]
Raw data (loadavg): 0.97 0.95 0.72 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57241 0 2 0 8507 238 0 0 25 0 1 0 1851762984 260673536 55394 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63641 55394 145 145 0 63496 0
[pid=24612] vsize: 254564
Current children cumulated CPU time (s) 87.46
Current children cumulated vsize (Kb) 256688

[startup+100.013 s]
Raw data (loadavg): 0.97 0.95 0.72 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57331 0 2 0 9506 239 0 0 25 0 1 0 1851762984 261046272 55484 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63732 55484 145 145 0 63587 0
[pid=24612] vsize: 254928
Current children cumulated CPU time (s) 97.46
Current children cumulated vsize (Kb) 257052

[startup+110.015 s]
Raw data (loadavg): 0.97 0.95 0.72 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57415 0 2 0 10505 240 0 0 25 0 1 0 1851762984 261296128 55568 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63793 55568 145 145 0 63648 0
[pid=24612] vsize: 255172
Current children cumulated CPU time (s) 107.46
Current children cumulated vsize (Kb) 257296

[startup+120.016 s]
Raw data (loadavg): 0.98 0.95 0.72 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57481 0 2 0 11504 240 0 0 25 0 1 0 1851762984 261562368 55634 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63858 55634 145 145 0 63713 0
[pid=24612] vsize: 255432
Current children cumulated CPU time (s) 117.45
Current children cumulated vsize (Kb) 257556

[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57578 0 2 0 12503 240 0 0 25 0 1 0 1851762984 261963776 55731 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 63956 55731 145 145 0 63811 0
[pid=24612] vsize: 255824
Current children cumulated CPU time (s) 127.44
Current children cumulated vsize (Kb) 257948

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.73 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57637 0 2 0 13503 241 0 0 25 0 1 0 1851762984 262213632 55790 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64017 55790 145 145 0 63872 0
[pid=24612] vsize: 256068
Current children cumulated CPU time (s) 137.45
Current children cumulated vsize (Kb) 258192

[startup+150.019 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57714 0 2 0 14501 241 0 0 25 0 1 0 1851762984 262529024 55867 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64094 55867 145 145 0 63949 0
[pid=24612] vsize: 256376
Current children cumulated CPU time (s) 147.43
Current children cumulated vsize (Kb) 258500

[startup+160.02 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57802 0 2 0 15501 242 0 0 25 0 1 0 1851762984 262868992 55955 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64177 55955 145 145 0 64032 0
[pid=24612] vsize: 256708
Current children cumulated CPU time (s) 157.44
Current children cumulated vsize (Kb) 258832

[startup+170.02 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57855 0 2 0 16500 242 0 0 25 0 1 0 1851762984 263086080 56008 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64230 56008 145 145 0 64085 0
[pid=24612] vsize: 256920
Current children cumulated CPU time (s) 167.43
Current children cumulated vsize (Kb) 259044

[startup+180.02 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 57949 0 2 0 17500 243 0 0 25 0 1 0 1851762984 263467008 56102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64323 56102 145 145 0 64178 0
[pid=24612] vsize: 257292
Current children cumulated CPU time (s) 177.44
Current children cumulated vsize (Kb) 259416

[startup+190.022 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58017 0 2 0 18499 243 0 0 25 0 1 0 1851762984 263741440 56170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64390 56170 145 145 0 64245 0
[pid=24612] vsize: 257560
Current children cumulated CPU time (s) 187.43
Current children cumulated vsize (Kb) 259684

[startup+200.023 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58107 0 2 0 19497 244 0 0 25 0 1 0 1851762984 264110080 56260 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64480 56260 145 145 0 64335 0
[pid=24612] vsize: 257920
Current children cumulated CPU time (s) 197.42
Current children cumulated vsize (Kb) 260044

[startup+210.025 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58195 0 2 0 20496 244 0 0 25 0 1 0 1851762984 264466432 56348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64567 56348 145 145 0 64422 0
[pid=24612] vsize: 258268
Current children cumulated CPU time (s) 207.41
Current children cumulated vsize (Kb) 260392

[startup+220.025 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58292 0 2 0 21495 245 0 0 25 0 1 0 1851762984 264863744 56445 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64664 56445 145 145 0 64519 0
[pid=24612] vsize: 258656
Current children cumulated CPU time (s) 217.41
Current children cumulated vsize (Kb) 260780

[startup+230.025 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58369 0 2 0 22494 245 0 0 25 0 1 0 1851762984 265175040 56522 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64740 56522 145 145 0 64595 0
[pid=24612] vsize: 258960
Current children cumulated CPU time (s) 227.4
Current children cumulated vsize (Kb) 261084

[startup+240.026 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58432 0 2 0 23492 246 0 0 25 0 1 0 1851762984 265433088 56585 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64803 56585 145 145 0 64658 0
[pid=24612] vsize: 259212
Current children cumulated CPU time (s) 237.39
Current children cumulated vsize (Kb) 261336

[startup+250.027 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58508 0 2 0 24492 246 0 0 25 0 1 0 1851762984 265773056 56661 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64886 56661 145 145 0 64741 0
[pid=24612] vsize: 259544
Current children cumulated CPU time (s) 247.39
Current children cumulated vsize (Kb) 261668

[startup+260.028 s]
Raw data (loadavg): 1.06 0.98 0.76 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58582 0 2 0 25490 247 0 0 25 0 1 0 1851762984 266076160 56735 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 64960 56735 145 145 0 64815 0
[pid=24612] vsize: 259840
Current children cumulated CPU time (s) 257.38
Current children cumulated vsize (Kb) 261964

[startup+270.028 s]
Raw data (loadavg): 1.05 0.98 0.76 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58674 0 2 0 26489 248 0 0 25 0 1 0 1851762984 266342400 56827 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65025 56827 145 145 0 64880 0
[pid=24612] vsize: 260100
Current children cumulated CPU time (s) 267.38
Current children cumulated vsize (Kb) 262224

[startup+280.029 s]
Raw data (loadavg): 1.04 0.98 0.76 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58749 0 2 0 27488 248 0 0 25 0 1 0 1851762984 266645504 56902 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65099 56902 145 145 0 64954 0
[pid=24612] vsize: 260396
Current children cumulated CPU time (s) 277.37
Current children cumulated vsize (Kb) 262520

[startup+290.031 s]
Raw data (loadavg): 1.04 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58844 0 2 0 28488 249 0 0 25 0 1 0 1851762984 267034624 56997 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65194 56997 145 145 0 65049 0
[pid=24612] vsize: 260776
Current children cumulated CPU time (s) 287.38
Current children cumulated vsize (Kb) 262900

[startup+300.032 s]
Raw data (loadavg): 1.03 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 58949 0 2 0 29487 250 0 0 25 0 1 0 1851762984 267485184 57102 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65304 57102 145 145 0 65159 0
[pid=24612] vsize: 261216
Current children cumulated CPU time (s) 297.38
Current children cumulated vsize (Kb) 263340

[startup+310.032 s]
Raw data (loadavg): 1.03 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59079 0 2 0 30486 250 0 0 25 0 1 0 1851762984 267788288 57232 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65378 57232 145 145 0 65233 0
[pid=24612] vsize: 261512
Current children cumulated CPU time (s) 307.37
Current children cumulated vsize (Kb) 263636

[startup+320.033 s]
Raw data (loadavg): 1.02 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59167 0 2 0 31485 251 0 0 25 0 1 0 1851762984 268148736 57320 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65466 57320 145 145 0 65321 0
[pid=24612] vsize: 261864
Current children cumulated CPU time (s) 317.37
Current children cumulated vsize (Kb) 263988

[startup+330.034 s]
Raw data (loadavg): 1.02 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59251 0 2 0 32484 252 0 0 25 0 1 0 1851762984 268492800 57404 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65550 57404 145 145 0 65405 0
[pid=24612] vsize: 262200
Current children cumulated CPU time (s) 327.37
Current children cumulated vsize (Kb) 264324

[startup+340.035 s]
Raw data (loadavg): 1.01 0.98 0.77 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59367 0 2 0 33483 252 0 0 25 0 1 0 1851762984 268967936 57520 4294967295 134512640 135094434 3221224432 3221223024 134556866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65666 57520 145 145 0 65521 0
[pid=24612] vsize: 262664
Current children cumulated CPU time (s) 337.36
Current children cumulated vsize (Kb) 264788

[startup+350.036 s]
Raw data (loadavg): 1.01 0.98 0.78 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59470 0 2 0 34482 253 0 0 25 0 1 0 1851762984 269389824 57623 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65769 57623 145 145 0 65624 0
[pid=24612] vsize: 263076
Current children cumulated CPU time (s) 347.36
Current children cumulated vsize (Kb) 265200

[startup+360.036 s]
Raw data (loadavg): 1.01 0.98 0.78 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59588 0 2 0 35479 254 0 0 25 0 1 0 1851762984 269869056 57741 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 65886 57741 145 145 0 65741 0
[pid=24612] vsize: 263544
Current children cumulated CPU time (s) 357.34
Current children cumulated vsize (Kb) 265668

[startup+370.037 s]
Raw data (loadavg): 1.01 0.98 0.78 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59679 0 2 0 36478 254 0 0 25 0 1 0 1851762984 270241792 57832 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 65977 57832 145 145 0 65832 0
[pid=24612] vsize: 263908
Current children cumulated CPU time (s) 367.33
Current children cumulated vsize (Kb) 266032

[startup+380.037 s]
Raw data (loadavg): 1.01 0.98 0.78 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59729 0 2 0 37477 255 0 0 25 0 1 0 1851762984 270442496 57882 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66026 57882 145 145 0 65881 0
[pid=24612] vsize: 264104
Current children cumulated CPU time (s) 377.33
Current children cumulated vsize (Kb) 266228

[startup+390.039 s]
Raw data (loadavg): 1.00 0.98 0.78 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59794 0 2 0 38476 255 0 0 25 0 1 0 1851762984 270708736 57947 4294967295 134512640 135094434 3221224432 3221223024 134557143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66091 57947 145 145 0 65946 0
[pid=24612] vsize: 264364
Current children cumulated CPU time (s) 387.32
Current children cumulated vsize (Kb) 266488

[startup+400.039 s]
Raw data (loadavg): 1.00 0.98 0.79 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59847 0 2 0 39476 256 0 0 25 0 1 0 1851762984 270925824 58000 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66144 58000 145 145 0 65999 0
[pid=24612] vsize: 264576
Current children cumulated CPU time (s) 397.33
Current children cumulated vsize (Kb) 266700

[startup+410.04 s]
Raw data (loadavg): 1.00 0.98 0.79 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59919 0 2 0 40475 256 0 0 25 0 1 0 1851762984 271216640 58072 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66215 58072 145 145 0 66070 0
[pid=24612] vsize: 264860
Current children cumulated CPU time (s) 407.32
Current children cumulated vsize (Kb) 266984

[startup+420.041 s]
Raw data (loadavg): 1.00 0.98 0.79 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 59978 0 2 0 41475 256 0 0 25 0 1 0 1851762984 271458304 58131 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66274 58131 145 145 0 66129 0
[pid=24612] vsize: 265096
Current children cumulated CPU time (s) 417.32
Current children cumulated vsize (Kb) 267220

[startup+430.042 s]
Raw data (loadavg): 1.00 0.98 0.79 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60038 0 2 0 42474 257 0 0 25 0 1 0 1851762984 271704064 58191 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66334 58191 145 145 0 66189 0
[pid=24612] vsize: 265336
Current children cumulated CPU time (s) 427.32
Current children cumulated vsize (Kb) 267460

[startup+440.043 s]
Raw data (loadavg): 1.00 0.98 0.79 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60121 0 2 0 43473 257 0 0 25 0 1 0 1851762984 272039936 58274 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66416 58274 145 145 0 66271 0
[pid=24612] vsize: 265664
Current children cumulated CPU time (s) 437.31
Current children cumulated vsize (Kb) 267788

[startup+450.043 s]
Raw data (loadavg): 1.00 0.98 0.80 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60217 0 2 0 44472 258 0 0 25 0 1 0 1851762984 272433152 58370 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66512 58370 145 145 0 66367 0
[pid=24612] vsize: 266048
Current children cumulated CPU time (s) 447.31
Current children cumulated vsize (Kb) 268172

[startup+460.044 s]
Raw data (loadavg): 1.00 0.98 0.80 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60275 0 2 0 45471 259 0 0 25 0 1 0 1851762984 272670720 58428 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66570 58428 145 145 0 66425 0
[pid=24612] vsize: 266280
Current children cumulated CPU time (s) 457.31
Current children cumulated vsize (Kb) 268404

[startup+470.045 s]
Raw data (loadavg): 1.00 0.98 0.80 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60342 0 2 0 46470 259 0 0 25 0 1 0 1851762984 272941056 58495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66636 58495 145 145 0 66491 0
[pid=24612] vsize: 266544
Current children cumulated CPU time (s) 467.3
Current children cumulated vsize (Kb) 268668

[startup+480.046 s]
Raw data (loadavg): 1.00 0.98 0.80 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60443 0 2 0 47469 260 0 0 25 0 1 0 1851762984 273367040 58596 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66740 58596 145 145 0 66595 0
[pid=24612] vsize: 266960
Current children cumulated CPU time (s) 477.3
Current children cumulated vsize (Kb) 269084

[startup+490.048 s]
Raw data (loadavg): 1.00 0.98 0.80 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60560 0 2 0 48468 261 0 0 25 0 1 0 1851762984 273829888 58713 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66853 58713 145 145 0 66708 0
[pid=24612] vsize: 267412
Current children cumulated CPU time (s) 487.3
Current children cumulated vsize (Kb) 269536

[startup+500.047 s]
Raw data (loadavg): 1.00 0.98 0.81 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60643 0 2 0 49467 261 0 0 25 0 1 0 1851762984 274169856 58796 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 66936 58796 145 145 0 66791 0
[pid=24612] vsize: 267744
Current children cumulated CPU time (s) 497.29
Current children cumulated vsize (Kb) 269868

[startup+510.049 s]
Raw data (loadavg): 1.00 0.98 0.81 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60710 0 2 0 50466 262 0 0 25 0 1 0 1851762984 274505728 58863 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67018 58863 145 145 0 66873 0
[pid=24612] vsize: 268072
Current children cumulated CPU time (s) 507.29
Current children cumulated vsize (Kb) 270196

[startup+520.05 s]
Raw data (loadavg): 1.00 0.98 0.81 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60811 0 2 0 51465 263 0 0 25 0 1 0 1851762984 274919424 58964 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67119 58964 145 145 0 66974 0
[pid=24612] vsize: 268476
Current children cumulated CPU time (s) 517.29
Current children cumulated vsize (Kb) 270600

[startup+530.05 s]
Raw data (loadavg): 1.00 0.98 0.81 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60908 0 2 0 52464 263 0 0 25 0 1 0 1851762984 275312640 59061 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67215 59061 145 145 0 67070 0
[pid=24612] vsize: 268860
Current children cumulated CPU time (s) 527.28
Current children cumulated vsize (Kb) 270984

[startup+540.051 s]
Raw data (loadavg): 1.00 0.98 0.81 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 60985 0 2 0 53463 264 0 0 25 0 1 0 1851762984 275628032 59138 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67292 59138 145 145 0 67147 0
[pid=24612] vsize: 269168
Current children cumulated CPU time (s) 537.28
Current children cumulated vsize (Kb) 271292

[startup+550.051 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61074 0 2 0 54461 264 0 0 25 0 1 0 1851762984 275992576 59227 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67381 59227 145 145 0 67236 0
[pid=24612] vsize: 269524
Current children cumulated CPU time (s) 547.26
Current children cumulated vsize (Kb) 271648

[startup+560.052 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61124 0 2 0 55461 265 0 0 25 0 1 0 1851762984 276193280 59277 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67430 59277 145 145 0 67285 0
[pid=24612] vsize: 269720
Current children cumulated CPU time (s) 557.27
Current children cumulated vsize (Kb) 271844

[startup+570.053 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61176 0 2 0 56461 265 0 0 25 0 1 0 1851762984 276406272 59329 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67482 59329 145 145 0 67337 0
[pid=24612] vsize: 269928
Current children cumulated CPU time (s) 567.27
Current children cumulated vsize (Kb) 272052

[startup+580.054 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61242 0 2 0 57459 266 0 0 25 0 1 0 1851762984 276676608 59395 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67548 59395 145 145 0 67403 0
[pid=24612] vsize: 270192
Current children cumulated CPU time (s) 577.26
Current children cumulated vsize (Kb) 272316

[startup+590.055 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61332 0 2 0 58458 266 0 0 25 0 1 0 1851762984 277049344 59485 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67639 59485 145 145 0 67494 0
[pid=24612] vsize: 270556
Current children cumulated CPU time (s) 587.25
Current children cumulated vsize (Kb) 272680

[startup+600.055 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61409 0 2 0 59457 267 0 0 25 0 1 0 1851762984 277356544 59562 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67714 59562 145 145 0 67569 0
[pid=24612] vsize: 270856
Current children cumulated CPU time (s) 597.25
Current children cumulated vsize (Kb) 272980

[startup+610.056 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61492 0 2 0 60457 267 0 0 25 0 1 0 1851762984 277696512 59645 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67797 59645 145 145 0 67652 0
[pid=24612] vsize: 271188
Current children cumulated CPU time (s) 607.25
Current children cumulated vsize (Kb) 273312

[startup+620.057 s]
Raw data (loadavg): 1.00 0.98 0.82 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61574 0 2 0 61456 267 0 0 25 0 1 0 1851762984 278028288 59727 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67878 59727 145 145 0 67733 0
[pid=24612] vsize: 271512
Current children cumulated CPU time (s) 617.24
Current children cumulated vsize (Kb) 273636

[startup+630.058 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61678 0 2 0 62454 268 0 0 25 0 1 0 1851762984 278454272 59831 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 67982 59831 145 145 0 67837 0
[pid=24612] vsize: 271928
Current children cumulated CPU time (s) 627.23
Current children cumulated vsize (Kb) 274052

[startup+640.059 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61771 0 2 0 63453 268 0 0 25 0 1 0 1851762984 278835200 59924 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68075 59924 145 145 0 67930 0
[pid=24612] vsize: 272300
Current children cumulated CPU time (s) 637.22
Current children cumulated vsize (Kb) 274424

[startup+650.059 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61880 0 2 0 64452 268 0 0 25 0 1 0 1851762984 279277568 60033 4294967295 134512640 135094434 3221224432 3221223024 134557163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68183 60033 145 145 0 68038 0
[pid=24612] vsize: 272732
Current children cumulated CPU time (s) 647.21
Current children cumulated vsize (Kb) 274856

[startup+660.06 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 61988 0 2 0 65452 269 0 0 25 0 1 0 1851762984 279711744 60141 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68289 60141 145 145 0 68144 0
[pid=24612] vsize: 273156
Current children cumulated CPU time (s) 657.22
Current children cumulated vsize (Kb) 275280

[startup+670.061 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62072 0 2 0 66451 269 0 0 25 0 1 0 1851762984 280055808 60225 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68373 60225 145 145 0 68228 0
[pid=24612] vsize: 273492
Current children cumulated CPU time (s) 667.21
Current children cumulated vsize (Kb) 275616

[startup+680.061 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62157 0 2 0 67450 270 0 0 25 0 1 0 1851762984 280399872 60310 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68457 60310 145 145 0 68312 0
[pid=24612] vsize: 273828
Current children cumulated CPU time (s) 677.21
Current children cumulated vsize (Kb) 275952

[startup+690.063 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62234 0 2 0 68449 270 0 0 25 0 1 0 1851762984 280715264 60387 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68534 60387 145 145 0 68389 0
[pid=24612] vsize: 274136
Current children cumulated CPU time (s) 687.2
Current children cumulated vsize (Kb) 276260

[startup+700.064 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62284 0 2 0 69448 271 0 0 25 0 1 0 1851762984 280920064 60437 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68584 60437 145 145 0 68439 0
[pid=24612] vsize: 274336
Current children cumulated CPU time (s) 697.2
Current children cumulated vsize (Kb) 276460

[startup+710.064 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62345 0 2 0 70447 271 0 0 25 0 1 0 1851762984 281165824 60498 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68644 60498 145 145 0 68499 0
[pid=24612] vsize: 274576
Current children cumulated CPU time (s) 707.19
Current children cumulated vsize (Kb) 276700

[startup+720.065 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62447 0 2 0 71446 271 0 0 25 0 1 0 1851762984 281583616 60600 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68746 60600 145 145 0 68601 0
[pid=24612] vsize: 274984
Current children cumulated CPU time (s) 717.18
Current children cumulated vsize (Kb) 277108

[startup+730.066 s]
Raw data (loadavg): 1.00 0.98 0.83 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62528 0 2 0 72445 272 0 0 25 0 1 0 1851762984 281915392 60681 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68827 60681 145 145 0 68682 0
[pid=24612] vsize: 275308
Current children cumulated CPU time (s) 727.18
Current children cumulated vsize (Kb) 277432

[startup+740.067 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62590 0 2 0 73445 272 0 0 25 0 1 0 1851762984 282165248 60743 4294967295 134512640 135094434 3221224432 3221223024 134556845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68888 60743 145 145 0 68743 0
[pid=24612] vsize: 275552
Current children cumulated CPU time (s) 737.18
Current children cumulated vsize (Kb) 277676

[startup+750.068 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62663 0 2 0 74444 273 0 0 25 0 1 0 1851762984 282464256 60816 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 68961 60816 145 145 0 68816 0
[pid=24612] vsize: 275844
Current children cumulated CPU time (s) 747.18
Current children cumulated vsize (Kb) 277968

[startup+760.07 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62776 0 2 0 75443 273 0 0 25 0 1 0 1851762984 282927104 60929 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69074 60929 145 145 0 68929 0
[pid=24612] vsize: 276296
Current children cumulated CPU time (s) 757.17
Current children cumulated vsize (Kb) 278420

[startup+770.071 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62851 0 2 0 76442 274 0 0 25 0 1 0 1851762984 283230208 61004 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69148 61004 145 145 0 69003 0
[pid=24612] vsize: 276592
Current children cumulated CPU time (s) 767.17
Current children cumulated vsize (Kb) 278716

[startup+780.071 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 62925 0 2 0 77441 274 0 0 25 0 1 0 1851762984 283533312 61078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69222 61078 145 145 0 69077 0
[pid=24612] vsize: 276888
Current children cumulated CPU time (s) 777.16
Current children cumulated vsize (Kb) 279012

[startup+790.072 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63019 0 2 0 78440 275 0 0 25 0 1 0 1851762984 283918336 61172 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69316 61172 145 145 0 69171 0
[pid=24612] vsize: 277264
Current children cumulated CPU time (s) 787.16
Current children cumulated vsize (Kb) 279388

[startup+800.073 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63072 0 2 0 79439 275 0 0 25 0 1 0 1851762984 284131328 61225 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 69368 61225 145 145 0 69223 0
[pid=24612] vsize: 277472
Current children cumulated CPU time (s) 797.15
Current children cumulated vsize (Kb) 279596

[startup+810.075 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63150 0 2 0 80436 277 0 0 25 0 1 0 1851762984 284450816 61303 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69446 61303 145 145 0 69301 0
[pid=24612] vsize: 277784
Current children cumulated CPU time (s) 807.14
Current children cumulated vsize (Kb) 279908

[startup+820.076 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63237 0 2 0 81435 278 0 0 25 0 1 0 1851762984 284807168 61390 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69533 61390 145 145 0 69388 0
[pid=24612] vsize: 278132
Current children cumulated CPU time (s) 817.14
Current children cumulated vsize (Kb) 280256

[startup+830.077 s]
Raw data (loadavg): 1.00 0.98 0.84 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63313 0 2 0 82434 278 0 0 25 0 1 0 1851762984 285118464 61466 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69609 61466 145 145 0 69464 0
[pid=24612] vsize: 278436
Current children cumulated CPU time (s) 827.13
Current children cumulated vsize (Kb) 280560

[startup+840.077 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63437 0 2 0 83432 279 0 0 25 0 1 0 1851762984 285622272 61590 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69732 61590 145 145 0 69587 0
[pid=24612] vsize: 278928
Current children cumulated CPU time (s) 837.12
Current children cumulated vsize (Kb) 281052

[startup+850.078 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63500 0 2 0 84431 279 0 0 25 0 1 0 1851762984 285880320 61653 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69795 61653 145 145 0 69650 0
[pid=24612] vsize: 279180
Current children cumulated CPU time (s) 847.11
Current children cumulated vsize (Kb) 281304

[startup+860.079 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63558 0 2 0 85431 279 0 0 25 0 1 0 1851762984 286117888 61711 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69853 61711 145 145 0 69708 0
[pid=24612] vsize: 279412
Current children cumulated CPU time (s) 857.11
Current children cumulated vsize (Kb) 281536

[startup+870.08 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63633 0 2 0 86430 280 0 0 25 0 1 0 1851762984 286420992 61786 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69927 61786 145 145 0 69782 0
[pid=24612] vsize: 279708
Current children cumulated CPU time (s) 867.11
Current children cumulated vsize (Kb) 281832

[startup+880.081 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63692 0 2 0 87429 281 0 0 25 0 1 0 1851762984 286662656 61845 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 69986 61845 145 145 0 69841 0
[pid=24612] vsize: 279944
Current children cumulated CPU time (s) 877.11
Current children cumulated vsize (Kb) 282068

[startup+890.082 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63759 0 2 0 88428 281 0 0 25 0 1 0 1851762984 286937088 61912 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 70053 61912 145 145 0 69908 0
[pid=24612] vsize: 280212
Current children cumulated CPU time (s) 887.1
Current children cumulated vsize (Kb) 282336

[startup+900.083 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63827 0 2 0 89427 282 0 0 25 0 1 0 1851762984 287211520 61980 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 70120 61980 145 145 0 69975 0
[pid=24612] vsize: 280480
Current children cumulated CPU time (s) 897.1
Current children cumulated vsize (Kb) 282604

[startup+910.084 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63905 0 2 0 90425 283 0 0 25 0 1 0 1851762984 287531008 62058 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 70198 62058 145 145 0 70053 0
[pid=24612] vsize: 280792
Current children cumulated CPU time (s) 907.09
Current children cumulated vsize (Kb) 282916

[startup+920.085 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 63975 0 2 0 91424 283 0 0 25 0 1 0 1851762984 287817728 62128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 70268 62128 145 145 0 70123 0
[pid=24612] vsize: 281072
Current children cumulated CPU time (s) 917.08
Current children cumulated vsize (Kb) 283196

[startup+930.085 s]
Raw data (loadavg): 1.00 0.98 0.85 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64043 0 2 0 92423 284 0 0 25 0 1 0 1851762984 288096256 62196 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70336 62196 145 145 0 70191 0
[pid=24612] vsize: 281344
Current children cumulated CPU time (s) 927.08
Current children cumulated vsize (Kb) 283468

[startup+940.087 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64164 0 2 0 93421 285 0 0 25 0 1 0 1851762984 288587776 62317 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70456 62317 145 145 0 70311 0
[pid=24612] vsize: 281824
Current children cumulated CPU time (s) 937.07
Current children cumulated vsize (Kb) 283948

[startup+950.088 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64241 0 2 0 94419 286 0 0 25 0 1 0 1851762984 288903168 62394 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70533 62394 145 145 0 70388 0
[pid=24612] vsize: 282132
Current children cumulated CPU time (s) 947.06
Current children cumulated vsize (Kb) 284256

[startup+960.089 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64373 0 2 0 95417 287 0 0 25 0 1 0 1851762984 289443840 62526 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70665 62526 145 145 0 70520 0
[pid=24612] vsize: 282660
Current children cumulated CPU time (s) 957.05
Current children cumulated vsize (Kb) 284784

[startup+970.091 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64450 0 2 0 96415 289 0 0 25 0 1 0 1851762984 289755136 62603 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70741 62603 145 145 0 70596 0
[pid=24612] vsize: 282964
Current children cumulated CPU time (s) 967.05
Current children cumulated vsize (Kb) 285088

[startup+980.092 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64542 0 2 0 97414 289 0 0 25 0 1 0 1851762984 290131968 62695 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70833 62695 145 145 0 70688 0
[pid=24612] vsize: 283332
Current children cumulated CPU time (s) 977.04
Current children cumulated vsize (Kb) 285456

[startup+990.094 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64626 0 2 0 98412 290 0 0 25 0 1 0 1851762984 290476032 62779 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70917 62779 145 145 0 70772 0
[pid=24612] vsize: 283668
Current children cumulated CPU time (s) 987.03
Current children cumulated vsize (Kb) 285792

[startup+1000.1 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64702 0 2 0 99411 292 0 0 25 0 1 0 1851762984 290787328 62855 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 70993 62855 145 145 0 70848 0
[pid=24612] vsize: 283972
Current children cumulated CPU time (s) 997.04
Current children cumulated vsize (Kb) 286096

[startup+1010.1 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64808 0 2 0 100408 293 0 0 25 0 1 0 1851762984 291221504 62961 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71099 62961 145 145 0 70954 0
[pid=24612] vsize: 284396
Current children cumulated CPU time (s) 1007.02
Current children cumulated vsize (Kb) 286520

[startup+1020.1 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64876 0 2 0 101407 294 0 0 25 0 1 0 1851762984 291627008 63029 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71198 63029 145 145 0 71053 0
[pid=24612] vsize: 284792
Current children cumulated CPU time (s) 1017.02
Current children cumulated vsize (Kb) 286916

[startup+1030.1 s]
Raw data (loadavg): 1.00 0.98 0.86 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 64959 0 2 0 102405 295 0 0 25 0 1 0 1851762984 291966976 63112 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71281 63112 145 145 0 71136 0
[pid=24612] vsize: 285124
Current children cumulated CPU time (s) 1027.01
Current children cumulated vsize (Kb) 287248

[startup+1040.1 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65030 0 2 0 103403 295 0 0 25 0 1 0 1851762984 292257792 63183 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71352 63183 145 145 0 71207 0
[pid=24612] vsize: 285408
Current children cumulated CPU time (s) 1036.99
Current children cumulated vsize (Kb) 287532

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65105 0 2 0 104402 296 0 0 25 0 1 0 1851762984 292560896 63258 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71426 63258 145 145 0 71281 0
[pid=24612] vsize: 285704
Current children cumulated CPU time (s) 1046.99
Current children cumulated vsize (Kb) 287828

[startup+1060.1 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65213 0 2 0 105401 297 0 0 25 0 1 0 1851762984 293003264 63366 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71534 63366 145 145 0 71389 0
[pid=24612] vsize: 286136
Current children cumulated CPU time (s) 1056.99
Current children cumulated vsize (Kb) 288260

[startup+1070.1 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65290 0 2 0 106399 298 0 0 25 0 1 0 1851762984 293318656 63443 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71611 63443 145 145 0 71466 0
[pid=24612] vsize: 286444
Current children cumulated CPU time (s) 1066.98
Current children cumulated vsize (Kb) 288568

[startup+1080.1 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65366 0 2 0 107397 299 0 0 25 0 1 0 1851762984 293625856 63519 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71686 63519 145 145 0 71541 0
[pid=24612] vsize: 286744
Current children cumulated CPU time (s) 1076.97
Current children cumulated vsize (Kb) 288868

[startup+1090.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65423 0 2 0 108396 300 0 0 25 0 1 0 1851762984 293859328 63576 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71743 63576 145 145 0 71598 0
[pid=24612] vsize: 286972
Current children cumulated CPU time (s) 1086.97
Current children cumulated vsize (Kb) 289096

[startup+1100.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65496 0 2 0 109395 301 0 0 25 0 1 0 1851762984 294158336 63649 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71816 63649 145 145 0 71671 0
[pid=24612] vsize: 287264
Current children cumulated CPU time (s) 1096.97
Current children cumulated vsize (Kb) 289388

[startup+1110.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65562 0 2 0 110393 302 0 0 25 0 1 0 1851762984 294424576 63715 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24612/statm): 71881 63715 145 145 0 71736 0
[pid=24612] vsize: 287524
Current children cumulated CPU time (s) 1106.96
Current children cumulated vsize (Kb) 289648

[startup+1120.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65645 0 2 0 111391 303 0 0 25 0 1 0 1851762984 294764544 63798 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 71964 63798 145 145 0 71819 0
[pid=24612] vsize: 287856
Current children cumulated CPU time (s) 1116.95
Current children cumulated vsize (Kb) 289980

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65739 0 2 0 112391 303 0 0 25 0 1 0 1851762984 295149568 63892 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72058 63892 145 145 0 71913 0
[pid=24612] vsize: 288232
Current children cumulated CPU time (s) 1126.95
Current children cumulated vsize (Kb) 290356

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.98 0.87 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65825 0 2 0 113390 304 0 0 25 0 1 0 1851762984 295501824 63978 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72144 63978 145 145 0 71999 0
[pid=24612] vsize: 288576
Current children cumulated CPU time (s) 1136.95
Current children cumulated vsize (Kb) 290700

[startup+1150.11 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 65929 0 2 0 114389 304 0 0 25 0 1 0 1851762984 295927808 64082 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72248 64082 145 145 0 72103 0
[pid=24612] vsize: 288992
Current children cumulated CPU time (s) 1146.94
Current children cumulated vsize (Kb) 291116

[startup+1160.11 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66001 0 2 0 115388 305 0 0 25 0 1 0 1851762984 296218624 64154 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72319 64154 145 145 0 72174 0
[pid=24612] vsize: 289276
Current children cumulated CPU time (s) 1156.94
Current children cumulated vsize (Kb) 291400

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66078 0 2 0 116387 305 0 0 25 0 1 0 1851762984 296534016 64231 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72396 64231 145 145 0 72251 0
[pid=24612] vsize: 289584
Current children cumulated CPU time (s) 1166.93
Current children cumulated vsize (Kb) 291708

[startup+1180.11 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66142 0 2 0 117386 306 0 0 25 0 1 0 1851762984 296792064 64295 4294967295 134512640 135094434 3221224432 3221223024 134556996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72459 64295 145 145 0 72314 0
[pid=24612] vsize: 289836
Current children cumulated CPU time (s) 1176.93
Current children cumulated vsize (Kb) 291960

[startup+1190.12 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66280 0 2 0 118385 306 0 0 25 0 1 0 1851762984 297357312 64433 4294967295 134512640 135094434 3221224432 3221223024 134556906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72597 64433 145 145 0 72452 0
[pid=24612] vsize: 290388
Current children cumulated CPU time (s) 1186.92
Current children cumulated vsize (Kb) 292512

[startup+1200.12 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66356 0 2 0 119384 307 0 0 25 0 1 0 1851762984 297672704 64509 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72674 64509 145 145 0 72529 0
[pid=24612] vsize: 290696
Current children cumulated CPU time (s) 1196.92
Current children cumulated vsize (Kb) 292820

[startup+1210.12 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66430 0 2 0 120382 307 0 0 25 0 1 0 1851762984 297967616 64583 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72746 64583 145 145 0 72601 0
[pid=24612] vsize: 290984
Current children cumulated CPU time (s) 1206.9
Current children cumulated vsize (Kb) 293108



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 0.98 0.88 2/57 24612
Raw data (/proc/24608/stat): 24608 (minisat+_script) S 24607 24608 5929 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1851762979 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24608/statm): 531 226 485 147 0 384 0
[pid=24608] vsize: 2124
Raw data (/proc/24612/stat): 24612 (minisat+_64-bit) R 24608 24608 5929 0 -1 0 66430 0 2 0 120382 307 0 0 25 0 1 0 1851762984 297967616 64583 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24612/statm): 72746 64583 145 145 0 72601 0
[pid=24612] vsize: 290984
Current children cumulated CPU time (s) 1206.9
Current children cumulated vsize (Kb) 293108

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

Child status: 0
Real time (s): 1210.24
CPU time (s): 1207.03
CPU user time (s): 1203.83
CPU system time (s): 3.20451
CPU usage (%): 99.7347
Max. virtual memory (cumulated for all children) (Kb): 293108

Verifier Data

ERROR: no interpretation found !